code identifier namings are no longer imperative
authorhaftmann
Wed Oct 22 14:15:45 2008 +0200 (2008-10-22)
changeset 28663bd8438543bf2
parent 28662 64ab5bb68d4c
child 28664 d89ac2917157
code identifier namings are no longer imperative
src/HOL/HOL.thy
src/HOL/Library/Heap_Monad.thy
src/HOL/List.thy
src/HOL/Tools/numeral.ML
src/HOL/ex/Codegenerator_Pretty.thy
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_name.ML
src/Tools/code/code_printer.ML
src/Tools/code/code_target.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 22 14:15:44 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 22 14:15:45 2008 +0200
     1.3 @@ -1692,8 +1692,7 @@
     1.4  use "~~/src/HOL/Tools/recfun_codegen.ML"
     1.5  
     1.6  setup {*
     1.7 -  Code_Name.setup
     1.8 -  #> Code_ML.setup
     1.9 +  Code_ML.setup
    1.10    #> Code_Haskell.setup
    1.11    #> Nbe.setup
    1.12    #> Codegen.setup
     2.1 --- a/src/HOL/Library/Heap_Monad.thy	Wed Oct 22 14:15:44 2008 +0200
     2.2 +++ b/src/HOL/Library/Heap_Monad.thy	Wed Oct 22 14:15:45 2008 +0200
     2.3 @@ -296,66 +296,66 @@
     2.4  code_const "Heap_Monad.Fail" (OCaml "Failure")
     2.5  code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
     2.6  
     2.7 -ML {*
     2.8 -local
     2.9 +setup {* let
    2.10 +  open Code_Thingol;
    2.11  
    2.12 -open Code_Thingol;
    2.13 -
    2.14 -val bind' = Code_Name.const @{theory} @{const_name bindM};
    2.15 -val return' = Code_Name.const @{theory} @{const_name return};
    2.16 -val unit' = Code_Name.const @{theory} @{const_name Unity};
    2.17 +  fun lookup naming = the o Code_Thingol.lookup_const naming;
    2.18  
    2.19 -fun imp_monad_bind'' ts =
    2.20 -  let
    2.21 -    val dummy_name = "";
    2.22 -    val dummy_type = ITyVar dummy_name;
    2.23 -    val dummy_case_term = IVar dummy_name;
    2.24 -    (*assumption: dummy values are not relevant for serialization*)
    2.25 -    val unitt = IConst (unit', ([], []));
    2.26 -    fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    2.27 -      | dest_abs (t, ty) =
    2.28 -          let
    2.29 -            val vs = Code_Thingol.fold_varnames cons t [];
    2.30 -            val v = Name.variant vs "x";
    2.31 -            val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
    2.32 -          in ((v, ty'), t `$ IVar v) end;
    2.33 -    fun force (t as IConst (c, _) `$ t') = if c = return'
    2.34 -          then t' else t `$ unitt
    2.35 -      | force t = t `$ unitt;
    2.36 -    fun tr_bind' [(t1, _), (t2, ty2)] =
    2.37 -      let
    2.38 -        val ((v, ty), t) = dest_abs (t2, ty2);
    2.39 -      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    2.40 -    and tr_bind'' t = case Code_Thingol.unfold_app t
    2.41 -         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    2.42 -              then tr_bind' [(x1, ty1), (x2, ty2)]
    2.43 -              else force t
    2.44 -          | _ => force t;
    2.45 -  in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
    2.46 -    [(unitt, tr_bind' ts)]), dummy_case_term) end
    2.47 -and imp_monad_bind' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
    2.48 -   of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    2.49 -    | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    2.50 -    | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
    2.51 -  else IConst const `$$ map imp_monad_bind ts
    2.52 -and imp_monad_bind (IConst const) = imp_monad_bind' const []
    2.53 -  | imp_monad_bind (t as IVar _) = t
    2.54 -  | imp_monad_bind (t as _ `$ _) = (case unfold_app t
    2.55 -     of (IConst const, ts) => imp_monad_bind' const ts
    2.56 -      | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
    2.57 -  | imp_monad_bind (v_ty `|-> t) = v_ty `|-> imp_monad_bind t
    2.58 -  | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
    2.59 -      (((imp_monad_bind t, ty), (map o pairself) imp_monad_bind pats), imp_monad_bind t0);
    2.60 +  fun imp_monad_bind'' bind' return' unit' ts =
    2.61 +    let
    2.62 +      val dummy_name = "";
    2.63 +      val dummy_type = ITyVar dummy_name;
    2.64 +      val dummy_case_term = IVar dummy_name;
    2.65 +      (*assumption: dummy values are not relevant for serialization*)
    2.66 +      val unitt = IConst (unit', ([], []));
    2.67 +      fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    2.68 +        | dest_abs (t, ty) =
    2.69 +            let
    2.70 +              val vs = Code_Thingol.fold_varnames cons t [];
    2.71 +              val v = Name.variant vs "x";
    2.72 +              val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
    2.73 +            in ((v, ty'), t `$ IVar v) end;
    2.74 +      fun force (t as IConst (c, _) `$ t') = if c = return'
    2.75 +            then t' else t `$ unitt
    2.76 +        | force t = t `$ unitt;
    2.77 +      fun tr_bind' [(t1, _), (t2, ty2)] =
    2.78 +        let
    2.79 +          val ((v, ty), t) = dest_abs (t2, ty2);
    2.80 +        in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    2.81 +      and tr_bind'' t = case Code_Thingol.unfold_app t
    2.82 +           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    2.83 +                then tr_bind' [(x1, ty1), (x2, ty2)]
    2.84 +                else force t
    2.85 +            | _ => force t;
    2.86 +    in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
    2.87 +      [(unitt, tr_bind' ts)]), dummy_case_term) end
    2.88 +  and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
    2.89 +     of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
    2.90 +      | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
    2.91 +      | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
    2.92 +    else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
    2.93 +  and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
    2.94 +    | imp_monad_bind bind' return' unit' (t as IVar _) = t
    2.95 +    | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
    2.96 +       of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
    2.97 +        | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
    2.98 +    | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
    2.99 +    | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
   2.100 +        (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
   2.101 +
   2.102 +   fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
   2.103 +     (imp_monad_bind (lookup naming @{const_name bindM})
   2.104 +       (lookup naming @{const_name return})
   2.105 +       (lookup naming @{const_name Unity}));
   2.106  
   2.107  in
   2.108  
   2.109 -val imp_program = (Graph.map_nodes o map_terms_stmt) imp_monad_bind;
   2.110 +  Code_Target.extend_target ("SML_imp", ("SML", imp_program))
   2.111 +  #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
   2.112  
   2.113  end
   2.114  *}
   2.115  
   2.116 -setup {* Code_Target.extend_target ("SML_imp", ("SML", imp_program)) *}
   2.117 -setup {* Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
   2.118  
   2.119  code_reserved OCaml Failure raise
   2.120  
     3.1 --- a/src/HOL/List.thy	Wed Oct 22 14:15:44 2008 +0200
     3.2 +++ b/src/HOL/List.thy	Wed Oct 22 14:15:45 2008 +0200
     3.3 @@ -3520,20 +3520,8 @@
     3.4  local
     3.5  
     3.6  open Basic_Code_Thingol;
     3.7 -val nil' = Code_Name.const @{theory} @{const_name Nil};
     3.8 -val cons' = Code_Name.const @{theory} @{const_name Cons};
     3.9 -val char' = Code_Name.const @{theory} @{const_name Char}
    3.10 -val nibbles' = map (Code_Name.const @{theory})
    3.11 -   [@{const_name Nibble0}, @{const_name Nibble1},
    3.12 -    @{const_name Nibble2}, @{const_name Nibble3},
    3.13 -    @{const_name Nibble4}, @{const_name Nibble5},
    3.14 -    @{const_name Nibble6}, @{const_name Nibble7},
    3.15 -    @{const_name Nibble8}, @{const_name Nibble9},
    3.16 -    @{const_name NibbleA}, @{const_name NibbleB},
    3.17 -    @{const_name NibbleC}, @{const_name NibbleD},
    3.18 -    @{const_name NibbleE}, @{const_name NibbleF}];
    3.19 -
    3.20 -fun implode_list t =
    3.21 +
    3.22 +fun implode_list (nil', cons') t =
    3.23    let
    3.24      fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
    3.25            if c = cons'
    3.26 @@ -3546,19 +3534,19 @@
    3.27      | _ => NONE
    3.28    end;
    3.29  
    3.30 -fun decode_char (IConst (c1, _), IConst (c2, _)) =
    3.31 +fun decode_char nibbles' (IConst (c1, _), IConst (c2, _)) =
    3.32        let
    3.33          fun idx c = find_index (curry (op =) c) nibbles';
    3.34          fun decode ~1 _ = NONE
    3.35            | decode _ ~1 = NONE
    3.36            | decode n m = SOME (chr (n * 16 + m));
    3.37        in decode (idx c1) (idx c2) end
    3.38 -  | decode_char _ = NONE;
    3.39 -
    3.40 -fun implode_string mk_char mk_string ts =
    3.41 +  | decode_char _ _ = NONE;
    3.42 +
    3.43 +fun implode_string (char', nibbles') mk_char mk_string ts =
    3.44    let
    3.45      fun implode_char (IConst (c, _) `$ t1 `$ t2) =
    3.46 -          if c = char' then decode_char (t1, t2) else NONE
    3.47 +          if c = char' then decode_char nibbles' (t1, t2) else NONE
    3.48        | implode_char _ = NONE;
    3.49      val ts' = map implode_char ts;
    3.50    in if forall is_some ts'
    3.51 @@ -3566,6 +3554,20 @@
    3.52      else NONE
    3.53    end;
    3.54  
    3.55 +fun list_names naming = pairself (the o Code_Thingol.lookup_const naming)
    3.56 +  (@{const_name Nil}, @{const_name Cons});
    3.57 +fun char_name naming = (the o Code_Thingol.lookup_const naming)
    3.58 +  @{const_name Char}
    3.59 +fun nibble_names naming = map (the o Code_Thingol.lookup_const naming)
    3.60 +  [@{const_name Nibble0}, @{const_name Nibble1},
    3.61 +   @{const_name Nibble2}, @{const_name Nibble3},
    3.62 +   @{const_name Nibble4}, @{const_name Nibble5},
    3.63 +   @{const_name Nibble6}, @{const_name Nibble7},
    3.64 +   @{const_name Nibble8}, @{const_name Nibble9},
    3.65 +   @{const_name NibbleA}, @{const_name NibbleB},
    3.66 +   @{const_name NibbleC}, @{const_name NibbleD},
    3.67 +   @{const_name NibbleE}, @{const_name NibbleF}];
    3.68 +
    3.69  fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
    3.70    Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
    3.71      pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
    3.72 @@ -3576,8 +3578,8 @@
    3.73  fun pretty_list literals =
    3.74    let
    3.75      val mk_list = Code_Printer.literal_list literals;
    3.76 -    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
    3.77 -      case Option.map (cons t1) (implode_list t2)
    3.78 +    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
    3.79 +      case Option.map (cons t1) (implode_list (list_names naming) t2)
    3.80         of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
    3.81          | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    3.82    in (2, pretty) end;
    3.83 @@ -3587,9 +3589,9 @@
    3.84      val mk_list = Code_Printer.literal_list literals;
    3.85      val mk_char = Code_Printer.literal_char literals;
    3.86      val mk_string = Code_Printer.literal_string literals;
    3.87 -    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
    3.88 -      case Option.map (cons t1) (implode_list t2)
    3.89 -       of SOME ts => (case implode_string mk_char mk_string ts
    3.90 +    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
    3.91 +      case Option.map (cons t1) (implode_list (list_names naming) t2)
    3.92 +       of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
    3.93             of SOME p => p
    3.94              | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
    3.95          | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    3.96 @@ -3598,8 +3600,8 @@
    3.97  fun pretty_char literals =
    3.98    let
    3.99      val mk_char = Code_Printer.literal_char literals;
   3.100 -    fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
   3.101 -      case decode_char (t1, t2)
   3.102 +    fun pretty _ naming thm _ _ _ [(t1, _), (t2, _)] =
   3.103 +      case decode_char (nibble_names naming) (t1, t2)
   3.104         of SOME c => (Code_Printer.str o mk_char) c
   3.105          | NONE => Code_Printer.nerror thm "Illegal character expression";
   3.106    in (2, pretty) end;
   3.107 @@ -3608,9 +3610,9 @@
   3.108    let
   3.109      val mk_char = Code_Printer.literal_char literals;
   3.110      val mk_string = Code_Printer.literal_string literals;
   3.111 -    fun pretty _ thm _ _ _ [(t, _)] =
   3.112 -      case implode_list t
   3.113 -       of SOME ts => (case implode_string mk_char mk_string ts
   3.114 +    fun pretty _ naming thm _ _ _ [(t, _)] =
   3.115 +      case implode_list (list_names naming) t
   3.116 +       of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
   3.117             of SOME p => p
   3.118              | NONE => Code_Printer.nerror thm "Illegal message expression")
   3.119          | NONE => Code_Printer.nerror thm "Illegal message expression";
     4.1 --- a/src/HOL/Tools/numeral.ML	Wed Oct 22 14:15:44 2008 +0200
     4.2 +++ b/src/HOL/Tools/numeral.ML	Wed Oct 22 14:15:45 2008 +0200
     4.3 @@ -59,25 +59,28 @@
     4.4  
     4.5  fun add_code number_of negative unbounded target thy =
     4.6    let
     4.7 -    val pls' = Code_Name.const thy @{const_name Int.Pls};
     4.8 -    val min' = Code_Name.const thy @{const_name Int.Min};
     4.9 -    val bit0' = Code_Name.const thy @{const_name Int.Bit0};
    4.10 -    val bit1' = Code_Name.const thy @{const_name Int.Bit1};
    4.11      val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
    4.12 -    fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
    4.13 -          else if c = bit1' then 1
    4.14 -          else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
    4.15 -      | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
    4.16 -    fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
    4.17 -          else if c = min' then
    4.18 -            if negative then SOME ~1 else NONE
    4.19 -          else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
    4.20 -      | dest_numeral thm (t1 `$ t2) =
    4.21 -          let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
    4.22 -          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    4.23 -      | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
    4.24 -    fun pretty _ thm _ _ _ [(t, _)] =
    4.25 -      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
    4.26 +    fun dest_numeral naming thm =
    4.27 +      let
    4.28 +        val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
    4.29 +        val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
    4.30 +        val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
    4.31 +        val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
    4.32 +        fun dest_bit (IConst (c, _)) = if c = bit0' then 0
    4.33 +              else if c = bit1' then 1
    4.34 +              else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
    4.35 +          | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
    4.36 +        fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
    4.37 +              else if c = min' then
    4.38 +                if negative then SOME ~1 else NONE
    4.39 +              else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
    4.40 +          | dest_num (t1 `$ t2) =
    4.41 +              let val (n, b) = (dest_num t2, dest_bit t1)
    4.42 +              in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    4.43 +          | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
    4.44 +      in dest_num end;
    4.45 +    fun pretty _ naming thm _ _ _ [(t, _)] =
    4.46 +      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
    4.47    in
    4.48      thy
    4.49      |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
     5.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Wed Oct 22 14:15:44 2008 +0200
     5.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Wed Oct 22 14:15:45 2008 +0200
     5.3 @@ -17,7 +17,6 @@
     5.4  nonfix upto;
     5.5  *}
     5.6  
     5.7 -export_code "RType.*" -- "workaround for cache problem"
     5.8  export_code * in SML module_name CodegenTest
     5.9    in OCaml module_name CodegenTest file -
    5.10    in Haskell file -
     6.1 --- a/src/Tools/code/code_haskell.ML	Wed Oct 22 14:15:44 2008 +0200
     6.2 +++ b/src/Tools/code/code_haskell.ML	Wed Oct 22 14:15:45 2008 +0200
     6.3 @@ -32,7 +32,7 @@
     6.4        | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
     6.5    in gen_pr_bind pr_bind pr_term end;
     6.6  
     6.7 -fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
     6.8 +fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
     6.9      init_syms deresolve is_cons contr_classparam_typs deriving_show =
    6.10    let
    6.11      val deresolve_base = NameSpace.base o deresolve;
    6.12 @@ -42,24 +42,24 @@
    6.13      fun classparam_name class classparam = case syntax_class class
    6.14       of NONE => deresolve_base classparam
    6.15        | SOME (_, classparam_syntax) => case classparam_syntax classparam
    6.16 -         of NONE => (snd o dest_name) classparam
    6.17 +         of NONE => (snd o Code_Name.dest_name) classparam
    6.18            | SOME classparam => classparam;
    6.19      fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    6.20       of [] => []
    6.21        | classbinds => Pretty.enum "," "(" ")" (
    6.22            map (fn (v, class) =>
    6.23 -            str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
    6.24 +            str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
    6.25            @@ str " => ";
    6.26      fun pr_typforall tyvars vs = case map fst vs
    6.27       of [] => []
    6.28        | vnames => str "forall " :: Pretty.breaks
    6.29 -          (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    6.30 +          (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    6.31      fun pr_tycoexpr tyvars fxy (tyco, tys) =
    6.32        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
    6.33      and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
    6.34           of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
    6.35            | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
    6.36 -      | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    6.37 +      | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v;
    6.38      fun pr_typdecl tyvars (vs, tycoexpr) =
    6.39        Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
    6.40      fun pr_typscheme tyvars (vs, ty) =
    6.41 @@ -75,7 +75,7 @@
    6.42                    pr_term tyvars thm pat vars BR t2
    6.43                  ])
    6.44        | pr_term tyvars thm pat vars fxy (IVar v) =
    6.45 -          (str o lookup_var vars) v
    6.46 +          (str o Code_Name.lookup_var vars) v
    6.47        | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
    6.48            let
    6.49              val (binds, t') = Code_Thingol.unfold_abs t;
    6.50 @@ -102,7 +102,7 @@
    6.51              (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
    6.52            else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
    6.53          end
    6.54 -    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
    6.55 +    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons naming
    6.56      and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
    6.57      and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    6.58            let
    6.59 @@ -131,9 +131,9 @@
    6.60              ) (map pr bs)
    6.61            end
    6.62        | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
    6.63 -    fun pr_stmt (name, Code_Thingol.Fun ((vs, ty), [])) =
    6.64 +    fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
    6.65            let
    6.66 -            val tyvars = intro_vars (map fst vs) init_syms;
    6.67 +            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
    6.68              val n = (length o fst o Code_Thingol.unfold_fun) ty;
    6.69            in
    6.70              Pretty.chunks [
    6.71 @@ -153,10 +153,10 @@
    6.72                )
    6.73              ]
    6.74            end
    6.75 -      | pr_stmt (name, Code_Thingol.Fun ((vs, ty), raw_eqs)) =
    6.76 +      | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
    6.77            let
    6.78              val eqs = filter (snd o snd) raw_eqs;
    6.79 -            val tyvars = intro_vars (map fst vs) init_syms;
    6.80 +            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
    6.81              fun pr_eq ((ts, t), (thm, _)) =
    6.82                let
    6.83                  val consts = map_filter
    6.84 @@ -164,8 +164,8 @@
    6.85                      then NONE else (SOME o NameSpace.base o deresolve) c)
    6.86                      ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
    6.87                  val vars = init_syms
    6.88 -                  |> intro_vars consts
    6.89 -                  |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
    6.90 +                  |> Code_Name.intro_vars consts
    6.91 +                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
    6.92                         (insert (op =)) ts []);
    6.93                in
    6.94                  semicolon (
    6.95 @@ -186,18 +186,18 @@
    6.96                :: map pr_eq eqs
    6.97              )
    6.98            end
    6.99 -      | pr_stmt (name, Code_Thingol.Datatype (vs, [])) =
   6.100 +      | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
   6.101            let
   6.102 -            val tyvars = intro_vars (map fst vs) init_syms;
   6.103 +            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   6.104            in
   6.105              semicolon [
   6.106                str "data",
   6.107                pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
   6.108              ]
   6.109            end
   6.110 -      | pr_stmt (name, Code_Thingol.Datatype (vs, [(co, [ty])])) =
   6.111 +      | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
   6.112            let
   6.113 -            val tyvars = intro_vars (map fst vs) init_syms;
   6.114 +            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   6.115            in
   6.116              semicolon (
   6.117                str "newtype"
   6.118 @@ -208,9 +208,9 @@
   6.119                :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
   6.120              )
   6.121            end
   6.122 -      | pr_stmt (name, Code_Thingol.Datatype (vs, co :: cos)) =
   6.123 +      | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
   6.124            let
   6.125 -            val tyvars = intro_vars (map fst vs) init_syms;
   6.126 +            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   6.127              fun pr_co (co, tys) =
   6.128                concat (
   6.129                  (str o deresolve_base) co
   6.130 @@ -226,9 +226,9 @@
   6.131                @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
   6.132              )
   6.133            end
   6.134 -      | pr_stmt (name, Code_Thingol.Class (v, (superclasses, classparams))) =
   6.135 +      | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
   6.136            let
   6.137 -            val tyvars = intro_vars [v] init_syms;
   6.138 +            val tyvars = Code_Name.intro_vars [v] init_syms;
   6.139              fun pr_classparam (classparam, ty) =
   6.140                semicolon [
   6.141                  (str o classparam_name name) classparam,
   6.142 @@ -240,7 +240,7 @@
   6.143                Pretty.block [
   6.144                  str "class ",
   6.145                  Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
   6.146 -                str (deresolve_base name ^ " " ^ lookup_var tyvars v),
   6.147 +                str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
   6.148                  str " where {"
   6.149                ],
   6.150                str "};"
   6.151 @@ -248,7 +248,7 @@
   6.152            end
   6.153        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
   6.154            let
   6.155 -            val tyvars = intro_vars (map fst vs) init_syms;
   6.156 +            val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   6.157              fun pr_instdef ((classparam, c_inst), (thm, _)) =
   6.158                semicolon [
   6.159                  (str o classparam_name class) classparam,
   6.160 @@ -273,20 +273,20 @@
   6.161    let
   6.162      val module_alias = if is_some module_name then K module_name else raw_module_alias;
   6.163      val reserved_names = Name.make_context reserved_names;
   6.164 -    val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
   6.165 +    val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program;
   6.166      fun add_stmt (name, (stmt, deps)) =
   6.167        let
   6.168 -        val (module_name, base) = dest_name name;
   6.169 +        val (module_name, base) = Code_Name.dest_name name;
   6.170          val module_name' = mk_name_module module_name;
   6.171          val mk_name_stmt = yield_singleton Name.variants;
   6.172          fun add_fun upper (nsp_fun, nsp_typ) =
   6.173            let
   6.174              val (base', nsp_fun') =
   6.175 -              mk_name_stmt (if upper then first_upper base else base) nsp_fun
   6.176 +              mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun
   6.177            in (base', (nsp_fun', nsp_typ)) end;
   6.178          fun add_typ (nsp_fun, nsp_typ) =
   6.179            let
   6.180 -            val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
   6.181 +            val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ
   6.182            in (base', (nsp_fun, nsp_typ')) end;
   6.183          val add_name = case stmt
   6.184           of Code_Thingol.Fun _ => add_fun false
   6.185 @@ -314,15 +314,14 @@
   6.186      val hs_program = fold add_stmt (AList.make (fn name =>
   6.187        (Graph.get_node program name, Graph.imm_succs program name))
   6.188        (Graph.strong_conn program |> flat)) Symtab.empty;
   6.189 -    fun deresolver name =
   6.190 -      (fst o the o AList.lookup (op =) ((fst o snd o the
   6.191 -        o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
   6.192 -        handle Option => error ("Unknown statement name: " ^ labelled_name name);
   6.193 +    fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
   6.194 +      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name
   6.195 +      handle Option => error ("Unknown statement name: " ^ labelled_name name);
   6.196    in (deresolver, hs_program) end;
   6.197  
   6.198  fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
   6.199      reserved_names includes raw_module_alias
   6.200 -    syntax_class syntax_tyco syntax_const program cs destination =
   6.201 +    syntax_class syntax_tyco syntax_const naming program cs destination =
   6.202    let
   6.203      val stmt_names = Code_Target.stmt_names_of_destination destination;
   6.204      val module_name = if null stmt_names then raw_module_name else SOME "Code";
   6.205 @@ -335,16 +334,16 @@
   6.206          fun deriv _ "fun" = false
   6.207            | deriv tycos tyco = member (op =) tycos tyco orelse
   6.208                case try (Graph.get_node program) tyco
   6.209 -                of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
   6.210 +                of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
   6.211                      (maps snd cs)
   6.212                   | NONE => true
   6.213          and deriv' tycos (tyco `%% tys) = deriv tycos tyco
   6.214                andalso forall (deriv' tycos) tys
   6.215            | deriv' _ (ITyVar _) = true
   6.216        in deriv [] tyco end;
   6.217 -    val reserved_names = make_vars reserved_names;
   6.218 -    fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
   6.219 -      syntax_const labelled_name reserved_names
   6.220 +    val reserved_names = Code_Name.make_vars reserved_names;
   6.221 +    fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
   6.222 +      syntax_class syntax_tyco syntax_const reserved_names
   6.223        (if qualified then deresolver else NameSpace.base o deresolver)
   6.224        is_cons contr_classparam_typs
   6.225        (if string_classes then deriving_show else K false);
   6.226 @@ -432,14 +431,14 @@
   6.227       of SOME (((v, pat), ty), t') =>
   6.228            SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   6.229        | NONE => NONE;
   6.230 -    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   6.231 -          if c = c_bind then dest_bind t1 t2
   6.232 +    fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
   6.233 +          if c = c_bind_name then dest_bind t1 t2
   6.234            else NONE
   6.235 -      | dest_monad t = case Code_Thingol.split_let t
   6.236 +      | dest_monad _ t = case Code_Thingol.split_let t
   6.237           of SOME (((pat, ty), tbind), t') =>
   6.238                SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   6.239            | NONE => NONE;
   6.240 -    val implode_monad = Code_Thingol.unfoldr dest_monad;
   6.241 +    fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
   6.242      fun pr_monad pr_bind pr (NONE, t) vars =
   6.243            (semicolon [pr vars NOBR t], vars)
   6.244        | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
   6.245 @@ -448,9 +447,9 @@
   6.246        | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
   6.247            |> pr_bind NOBR bind
   6.248            |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   6.249 -    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   6.250 +    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   6.251       of SOME (bind, t') => let
   6.252 -          val (binds, t'') = implode_monad t'
   6.253 +          val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
   6.254            val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
   6.255          in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
   6.256        | NONE => brackify_infix (1, L) fxy
   6.257 @@ -460,11 +459,10 @@
   6.258  fun add_monad target' raw_c_bind thy =
   6.259    let
   6.260      val c_bind = Code_Unit.read_const thy raw_c_bind;
   6.261 -    val c_bind' = Code_Name.const thy c_bind;
   6.262    in if target = target' then
   6.263      thy
   6.264      |> Code_Target.add_syntax_const target c_bind
   6.265 -        (SOME (pretty_haskell_monad c_bind'))
   6.266 +        (SOME (pretty_haskell_monad c_bind))
   6.267    else error "Only Haskell target allows for monad syntax" end;
   6.268  
   6.269  
     7.1 --- a/src/Tools/code/code_ml.ML	Wed Oct 22 14:15:44 2008 +0200
     7.2 +++ b/src/Tools/code/code_ml.ML	Wed Oct 22 14:15:45 2008 +0200
     7.3 @@ -42,15 +42,15 @@
     7.4  
     7.5  (** SML serailizer **)
     7.6  
     7.7 -fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
     7.8 +fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
     7.9    let
    7.10      val pr_label_classrel = translate_string (fn "." => "__" | c => c)
    7.11        o NameSpace.qualifier;
    7.12      val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
    7.13      fun pr_dicts fxy ds =
    7.14        let
    7.15 -        fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
    7.16 -          | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
    7.17 +        fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
    7.18 +          | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
    7.19          fun pr_proj [] p =
    7.20                p
    7.21            | pr_proj [p'] p =
    7.22 @@ -86,7 +86,7 @@
    7.23      fun pr_term thm pat vars fxy (IConst c) =
    7.24            pr_app thm pat vars fxy (c, [])
    7.25        | pr_term thm pat vars fxy (IVar v) =
    7.26 -          str (lookup_var vars v)
    7.27 +          str (Code_Name.lookup_var vars v)
    7.28        | pr_term thm pat vars fxy (t as t1 `$ t2) =
    7.29            (case Code_Thingol.unfold_const_app t
    7.30             of SOME c_ts => pr_app thm pat vars fxy c_ts
    7.31 @@ -116,7 +116,7 @@
    7.32        else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
    7.33          (str o deresolve) c
    7.34            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
    7.35 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
    7.36 +    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
    7.37      and pr_bind' ((NONE, NONE), _) = str "_"
    7.38        | pr_bind' ((SOME v, NONE), _) = str v
    7.39        | pr_bind' ((NONE, SOME p), _) = p
    7.40 @@ -199,8 +199,8 @@
    7.41                              then NONE else (SOME o NameSpace.base o deresolve) c)
    7.42                              ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
    7.43                          val vars = reserved_names
    7.44 -                          |> intro_vars consts
    7.45 -                          |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
    7.46 +                          |> Code_Name.intro_vars consts
    7.47 +                          |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
    7.48                                 (insert (op =)) ts []);
    7.49                        in
    7.50                          concat (
    7.51 @@ -250,7 +250,7 @@
    7.52            in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
    7.53       | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
    7.54            let
    7.55 -            val w = first_upper v ^ "_";
    7.56 +            val w = Code_Name.first_upper v ^ "_";
    7.57              fun pr_superclass_field (class, classrel) =
    7.58                (concat o map str) [
    7.59                  pr_label_classrel classrel, ":", "'" ^ v, deresolve class
    7.60 @@ -342,12 +342,12 @@
    7.61  
    7.62  (** OCaml serializer **)
    7.63  
    7.64 -fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
    7.65 +fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    7.66    let
    7.67      fun pr_dicts fxy ds =
    7.68        let
    7.69 -        fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
    7.70 -          | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
    7.71 +        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
    7.72 +          | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
    7.73          fun pr_proj ps p =
    7.74            fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
    7.75          fun pr_dict fxy (DictConst (inst, dss)) =
    7.76 @@ -379,7 +379,7 @@
    7.77      fun pr_term thm pat vars fxy (IConst c) =
    7.78            pr_app thm pat vars fxy (c, [])
    7.79        | pr_term thm pat vars fxy (IVar v) =
    7.80 -          str (lookup_var vars v)
    7.81 +          str (Code_Name.lookup_var vars v)
    7.82        | pr_term thm pat vars fxy (t as t1 `$ t2) =
    7.83            (case Code_Thingol.unfold_const_app t
    7.84             of SOME c_ts => pr_app thm pat vars fxy c_ts
    7.85 @@ -407,7 +407,7 @@
    7.86          else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
    7.87        else (str o deresolve) c
    7.88          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
    7.89 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
    7.90 +    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
    7.91      and pr_bind' ((NONE, NONE), _) = str "_"
    7.92        | pr_bind' ((SOME v, NONE), _) = str v
    7.93        | pr_bind' ((NONE, SOME p), _) = p
    7.94 @@ -449,8 +449,8 @@
    7.95          val x = Name.variant (map_filter I fished1) "x";
    7.96          val fished2 = map_index (fillup_param x) fished1;
    7.97          val (fished3, _) = Name.variants fished2 Name.context;
    7.98 -        val vars' = intro_vars fished3 vars;
    7.99 -      in map (lookup_var vars') fished3 end;
   7.100 +        val vars' = Code_Name.intro_vars fished3 vars;
   7.101 +      in map (Code_Name.lookup_var vars') fished3 end;
   7.102      fun pr_stmt (MLFuns (funns as funn :: funns')) =
   7.103            let
   7.104              fun pr_eq ((ts, t), (thm, _)) =
   7.105 @@ -460,8 +460,8 @@
   7.106                      then NONE else (SOME o NameSpace.base o deresolve) c)
   7.107                      ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   7.108                  val vars = reserved_names
   7.109 -                  |> intro_vars consts
   7.110 -                  |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   7.111 +                  |> Code_Name.intro_vars consts
   7.112 +                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   7.113                        (insert (op =)) ts []);
   7.114                in concat [
   7.115                  (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   7.116 @@ -488,8 +488,8 @@
   7.117                          then NONE else (SOME o NameSpace.base o deresolve) c)
   7.118                          ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   7.119                      val vars = reserved_names
   7.120 -                      |> intro_vars consts
   7.121 -                      |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   7.122 +                      |> Code_Name.intro_vars consts
   7.123 +                      |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   7.124                            (insert (op =)) ts []);
   7.125                    in
   7.126                      concat (
   7.127 @@ -516,7 +516,7 @@
   7.128                          ((fold o Code_Thingol.fold_constnames)
   7.129                            (insert (op =)) (map (snd o fst) eqs) []);
   7.130                      val vars = reserved_names
   7.131 -                      |> intro_vars consts;
   7.132 +                      |> Code_Name.intro_vars consts;
   7.133                      val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
   7.134                    in
   7.135                      Pretty.block (
   7.136 @@ -574,7 +574,7 @@
   7.137            in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   7.138       | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   7.139            let
   7.140 -            val w = "_" ^ first_upper v;
   7.141 +            val w = "_" ^ Code_Name.first_upper v;
   7.142              fun pr_superclass_field (class, classrel) =
   7.143                (concat o map str) [
   7.144                  deresolve classrel, ":", "'" ^ v, deresolve class
   7.145 @@ -716,16 +716,16 @@
   7.146        let
   7.147          val (x, nsp_typ') = f nsp_typ
   7.148        in (x, (nsp_fun, nsp_typ')) end;
   7.149 -    val mk_name_module = mk_name_module reserved_names NONE module_alias program;
   7.150 +    val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
   7.151      fun mk_name_stmt upper name nsp =
   7.152        let
   7.153 -        val (_, base) = dest_name name;
   7.154 -        val base' = if upper then first_upper base else base;
   7.155 +        val (_, base) = Code_Name.dest_name name;
   7.156 +        val base' = if upper then Code_Name.first_upper base else base;
   7.157          val ([base''], nsp') = Name.variants [base'] nsp;
   7.158        in (base'', nsp') end;
   7.159      fun add_funs stmts =
   7.160        fold_map
   7.161 -        (fn (name, Code_Thingol.Fun stmt) =>
   7.162 +        (fn (name, Code_Thingol.Fun (_, stmt)) =>
   7.163                map_nsp_fun_yield (mk_name_stmt false name) #>>
   7.164                  rpair (name, stmt |> apsnd (filter (snd o snd)))
   7.165            | (name, _) =>
   7.166 @@ -734,7 +734,7 @@
   7.167        #>> (split_list #> apsnd MLFuns);
   7.168      fun add_datatypes stmts =
   7.169        fold_map
   7.170 -        (fn (name, Code_Thingol.Datatype stmt) =>
   7.171 +        (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   7.172                map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   7.173            | (name, Code_Thingol.Datatypecons _) =>
   7.174                map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   7.175 @@ -747,8 +747,8 @@
   7.176               | stmts => MLDatas stmts)));
   7.177      fun add_class stmts =
   7.178        fold_map
   7.179 -        (fn (name, Code_Thingol.Class info) =>
   7.180 -              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
   7.181 +        (fn (name, Code_Thingol.Class (_, stmt)) =>
   7.182 +              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   7.183            | (name, Code_Thingol.Classrel _) =>
   7.184                map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   7.185            | (name, Code_Thingol.Classparam _) =>
   7.186 @@ -786,7 +786,7 @@
   7.187            []
   7.188            |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   7.189            |> subtract (op =) names;
   7.190 -        val (module_names, _) = (split_list o map dest_name) names;
   7.191 +        val (module_names, _) = (split_list o map Code_Name.dest_name) names;
   7.192          val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   7.193            handle Empty =>
   7.194              error ("Different namespace prefixes for mutual dependencies:\n"
   7.195 @@ -796,7 +796,7 @@
   7.196          val module_name_path = NameSpace.explode module_name;
   7.197          fun add_dep name name' =
   7.198            let
   7.199 -            val module_name' = (mk_name_module o fst o dest_name) name';
   7.200 +            val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
   7.201            in if module_name = module_name' then
   7.202              map_node module_name_path (Graph.add_edge (name, name'))
   7.203            else let
   7.204 @@ -824,7 +824,7 @@
   7.205            (rev (Graph.strong_conn program)));
   7.206      fun deresolver prefix name = 
   7.207        let
   7.208 -        val module_name = (fst o dest_name) name;
   7.209 +        val module_name = (fst o Code_Name.dest_name) name;
   7.210          val module_name' = (NameSpace.explode o mk_name_module) module_name;
   7.211          val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   7.212          val stmt_name =
   7.213 @@ -840,19 +840,19 @@
   7.214    in (deresolver, nodes) end;
   7.215  
   7.216  fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
   7.217 -  _ syntax_tyco syntax_const program cs destination =
   7.218 +  _ syntax_tyco syntax_const naming program cs destination =
   7.219    let
   7.220      val is_cons = Code_Thingol.is_cons program;
   7.221      val stmt_names = Code_Target.stmt_names_of_destination destination;
   7.222      val module_name = if null stmt_names then raw_module_name else SOME "Code";
   7.223      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   7.224        reserved_names raw_module_alias program;
   7.225 -    val reserved_names = make_vars reserved_names;
   7.226 +    val reserved_names = Code_Name.make_vars reserved_names;
   7.227      fun pr_node prefix (Dummy _) =
   7.228            NONE
   7.229        | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
   7.230            (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
   7.231 -            (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
   7.232 +            (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
   7.233                (deresolver prefix) is_cons stmt)
   7.234            else NONE
   7.235        | pr_node prefix (Module (module_name, (_, nodes))) =
   7.236 @@ -861,8 +861,8 @@
   7.237                o rev o flat o Graph.strong_conn) nodes)
   7.238            |> (if null stmt_names then pr_module module_name else Pretty.chunks)
   7.239            |> SOME;
   7.240 -    val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
   7.241 -      cs;
   7.242 +    val cs' = (map o try)
   7.243 +      (deresolver (if is_some module_name then the_list module_name else [])) cs;
   7.244      val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
   7.245        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
   7.246    in
   7.247 @@ -877,8 +877,8 @@
   7.248  
   7.249  (** ML (system language) code for evaluation and instrumentalization **)
   7.250  
   7.251 -fun ml_code_of thy = Code_Target.serialize_custom thy
   7.252 -  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   7.253 +fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,
   7.254 +    (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   7.255    literals_sml));
   7.256  
   7.257  
   7.258 @@ -890,15 +890,16 @@
   7.259      val _ = if null (term_frees (term_of ct)) then () else error ("Term "
   7.260        ^ quote (Syntax.string_of_term_global thy (term_of ct))
   7.261        ^ " to be evaluated contains free variables");
   7.262 -    fun eval' program ((vs, ty), t) deps =
   7.263 +    fun eval' naming program ((vs, ty), t) deps =
   7.264        let
   7.265          val _ = if Code_Thingol.contains_dictvar t then
   7.266            error "Term to be evaluated constains free dictionaries" else ();
   7.267 +        val value_name = "Value.VALUE.value"
   7.268          val program' = program
   7.269 -          |> Graph.new_node (Code_Name.value_name,
   7.270 -              Code_Thingol.Fun (([], ty), [(([], t), (Drule.dummy_thm, true))]))
   7.271 -          |> fold (curry Graph.add_edge Code_Name.value_name) deps;
   7.272 -        val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
   7.273 +          |> Graph.new_node (value_name,
   7.274 +              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
   7.275 +          |> fold (curry Graph.add_edge value_name) deps;
   7.276 +        val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
   7.277          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
   7.278            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
   7.279        in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
   7.280 @@ -922,12 +923,13 @@
   7.281  
   7.282  fun delayed_code thy consts () =
   7.283    let
   7.284 -    val (consts', program) = Code_Thingol.consts_program thy consts;
   7.285 -    val (ml_code, consts'') = ml_code_of thy program consts';
   7.286 -    val _ = if length consts <> length consts'' then
   7.287 -      error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts)
   7.288 -        ^ "\nhas a user-defined serialization") else ();
   7.289 -  in (ml_code, consts ~~ consts'') end;
   7.290 +    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
   7.291 +    val (ml_code, consts'') = ml_code_of thy naming program consts';
   7.292 +    val const_tab = map2 (fn const => fn NONE =>
   7.293 +      error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
   7.294 +        ^ "\nhas a user-defined serialization")
   7.295 +      | SOME const' => (const, const')) consts consts''
   7.296 +  in (ml_code, const_tab) end;
   7.297  
   7.298  fun register_const const ctxt =
   7.299    let
     8.1 --- a/src/Tools/code/code_name.ML	Wed Oct 22 14:15:44 2008 +0200
     8.2 +++ b/src/Tools/code/code_name.ML	Wed Oct 22 14:15:45 2008 +0200
     8.3 @@ -2,62 +2,45 @@
     8.4      ID:         $Id$
     8.5      Author:     Florian Haftmann, TU Muenchen
     8.6  
     8.7 -Naming policies for code generation: prefixing any name by corresponding
     8.8 -theory name, conversion to alphanumeric representation.
     8.9 -Mappings are incrementally cached.  Assumes non-concurrent processing
    8.10 -inside a single theory.
    8.11 +Some code generator infrastructure concerning names.
    8.12  *)
    8.13  
    8.14  signature CODE_NAME =
    8.15  sig
    8.16 -  val read_const_exprs: theory -> string list -> string list * string list
    8.17 +  structure StringPairTab: TABLE
    8.18 +  val first_upper: string -> string
    8.19 +  val first_lower: string -> string
    8.20 +  val dest_name: string -> string * string
    8.21  
    8.22    val purify_var: string -> string
    8.23    val purify_tvar: string -> string
    8.24    val purify_sym: string -> string
    8.25 +  val purify_base: bool -> string -> string
    8.26    val check_modulename: string -> string
    8.27  
    8.28 -  val class: theory -> class -> class
    8.29 -  val class_rev: theory -> class -> class option
    8.30 -  val classrel: theory -> class * class -> string
    8.31 -  val classrel_rev: theory -> string -> (class * class) option
    8.32 -  val tyco: theory -> string -> string
    8.33 -  val tyco_rev: theory -> string -> string option
    8.34 -  val instance: theory -> class * string -> string
    8.35 -  val instance_rev: theory -> string -> (class * string) option
    8.36 -  val const: theory -> string -> string
    8.37 -  val const_rev: theory -> string -> string option
    8.38 -  val value_name: string
    8.39 -  val labelled_name: theory -> string -> string
    8.40 +  type var_ctxt
    8.41 +  val make_vars: string list -> var_ctxt
    8.42 +  val intro_vars: string list -> var_ctxt -> var_ctxt
    8.43 +  val lookup_var: var_ctxt -> string -> string
    8.44  
    8.45 -  val setup: theory -> theory
    8.46 +  val read_const_exprs: theory -> string list -> string list * string list
    8.47 +  val mk_name_module: Name.context -> string option -> (string -> string option)
    8.48 +    -> 'a Graph.T -> string -> string
    8.49  end;
    8.50  
    8.51  structure Code_Name: CODE_NAME =
    8.52  struct
    8.53  
    8.54 -(** constant expressions **)
    8.55 +(** auxiliary **)
    8.56 +
    8.57 +structure StringPairTab =
    8.58 +  TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
    8.59  
    8.60 -fun read_const_exprs thy =
    8.61 -  let
    8.62 -    fun consts_of some_thyname =
    8.63 -      let
    8.64 -        val thy' = case some_thyname
    8.65 -         of SOME thyname => ThyInfo.the_theory thyname thy
    8.66 -          | NONE => thy;
    8.67 -        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    8.68 -          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
    8.69 -        fun belongs_here c =
    8.70 -          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
    8.71 -      in case some_thyname
    8.72 -       of NONE => cs
    8.73 -        | SOME thyname => filter belongs_here cs
    8.74 -      end;
    8.75 -    fun read_const_expr "*" = ([], consts_of NONE)
    8.76 -      | read_const_expr s = if String.isSuffix ".*" s
    8.77 -          then ([], consts_of (SOME (unsuffix ".*" s)))
    8.78 -          else ([Code_Unit.read_const thy s], []);
    8.79 -  in pairself flat o split_list o map read_const_expr end;
    8.80 +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    8.81 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    8.82 +
    8.83 +val dest_name =
    8.84 +  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
    8.85  
    8.86  
    8.87  (** purification **)
    8.88 @@ -92,82 +75,16 @@
    8.89    | purify_tvar v =
    8.90        (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
    8.91  
    8.92 -fun check_modulename mn =
    8.93 -  let
    8.94 -    val mns = NameSpace.explode mn;
    8.95 -    val mns' = map (purify_name true false) mns;
    8.96 -  in
    8.97 -    if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
    8.98 -      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
    8.99 -  end;
   8.100 -
   8.101 -
   8.102 -(** global names (identifiers) **)
   8.103 -
   8.104 -(* identifier categories *)
   8.105 -
   8.106 -val suffix_class = "class";
   8.107 -val suffix_classrel = "classrel"
   8.108 -val suffix_tyco = "tyco";
   8.109 -val suffix_instance = "inst";
   8.110 -val suffix_const = "const";
   8.111 -
   8.112 -fun string_of_classrel (class, superclass) = class ^ " < " ^ superclass;
   8.113 -fun string_of_instance (class, tyco) = tyco ^ " :: " ^ class;
   8.114 -
   8.115 -fun add_suffix nsp name =
   8.116 -  NameSpace.append name nsp;
   8.117 -
   8.118 -fun dest_suffix nsp name =
   8.119 -  if NameSpace.base name = nsp
   8.120 -  then SOME (NameSpace.qualifier name)
   8.121 -  else NONE;
   8.122 -
   8.123 -local
   8.124 -
   8.125 -val name_mapping  = [
   8.126 -  (suffix_class,       "class"),
   8.127 -  (suffix_classrel,    "subclass relation"),
   8.128 -  (suffix_tyco,        "type constructor"),
   8.129 -  (suffix_instance,    "instance"),
   8.130 -  (suffix_const,       "constant")
   8.131 -]
   8.132 -
   8.133 -in
   8.134 -
   8.135 -val category_of = the o AList.lookup (op =) name_mapping o NameSpace.base;
   8.136 -
   8.137 -end;
   8.138 -
   8.139 -
   8.140 -(* theory name lookup *)
   8.141 -
   8.142 -local
   8.143 -  fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
   8.144 -in
   8.145 -  fun thyname_of_class thy =
   8.146 -    thyname_of thy (ProofContext.query_class (ProofContext.init thy));
   8.147 -  fun thyname_of_tyco thy =
   8.148 -    thyname_of thy (Type.the_tags (Sign.tsig_of thy));
   8.149 -  fun thyname_of_instance thy a = case AxClass.arity_property thy a Markup.theory_nameN
   8.150 -   of [] => error ("no such instance: " ^ (quote o string_of_instance) a)
   8.151 -    | thyname :: _ => thyname;
   8.152 -  fun thyname_of_const thy =
   8.153 -    thyname_of thy (Consts.the_tags (Sign.consts_of thy));
   8.154 -end;
   8.155 -
   8.156 -
   8.157 -(* naming policies *)
   8.158 -
   8.159  val purify_prefix =
   8.160    explode
   8.161 -  (*should disappear as soon as hierarchical theory name spaces are available*)
   8.162 +  (*FIMXE should disappear as soon as hierarchical theory name spaces are available*)
   8.163    #> Symbol.scanner "Malformed name"
   8.164        (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
   8.165    #> implode
   8.166    #> NameSpace.explode
   8.167    #> map (purify_name true false);
   8.168  
   8.169 +(*FIMXE non-canonical function treating non-canonical names*)
   8.170  fun purify_base _ "op &" = "and"
   8.171    | purify_base _ "op |" = "or"
   8.172    | purify_base _ "op -->" = "implies"
   8.173 @@ -183,227 +100,73 @@
   8.174  
   8.175  val purify_sym = purify_base false;
   8.176  
   8.177 -fun default_policy thy get_basename get_thyname name =
   8.178 +fun check_modulename mn =
   8.179    let
   8.180 -    val prefix = (purify_prefix o get_thyname thy) name;
   8.181 -    val base = (purify_base true o get_basename) name;
   8.182 -  in NameSpace.implode (prefix @ [base]) end;
   8.183 -
   8.184 -fun class_policy thy = default_policy thy NameSpace.base thyname_of_class;
   8.185 -fun classrel_policy thy = default_policy thy (fn (class1, class2) => 
   8.186 -  NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
   8.187 -  (*order fits nicely with composed projections*)
   8.188 -fun tyco_policy thy = default_policy thy NameSpace.base thyname_of_tyco;
   8.189 -fun instance_policy thy = default_policy thy (fn (class, tyco) => 
   8.190 -  NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
   8.191 -
   8.192 -fun force_thyname thy c = case Code.get_datatype_of_constr thy c
   8.193 - of SOME dtco => SOME (thyname_of_tyco thy dtco)
   8.194 -  | NONE => (case AxClass.class_of_param thy c
   8.195 -     of SOME class => SOME (thyname_of_class thy class)
   8.196 -      | NONE => (case AxClass.inst_of_param thy c
   8.197 -         of SOME (c, tyco) => SOME (thyname_of_instance thy
   8.198 -              ((the o AxClass.class_of_param thy) c, tyco))
   8.199 -          | NONE => NONE));
   8.200 -
   8.201 -fun const_policy thy c =
   8.202 -  case force_thyname thy c
   8.203 -   of NONE => default_policy thy NameSpace.base thyname_of_const c
   8.204 -    | SOME thyname => let
   8.205 -        val prefix = purify_prefix thyname;
   8.206 -        val base = (purify_base true o NameSpace.base) c;
   8.207 -      in NameSpace.implode (prefix @ [base]) end;
   8.208 -
   8.209 -
   8.210 -(* theory and code data *)
   8.211 -
   8.212 -type tyco = string;
   8.213 -type const = string;
   8.214 -
   8.215 -structure StringPairTab =
   8.216 -  TableFun(
   8.217 -    type key = string * string;
   8.218 -    val ord = prod_ord fast_string_ord fast_string_ord;
   8.219 -  );
   8.220 -
   8.221 -datatype names = Names of {
   8.222 -  class: class Symtab.table * class Symtab.table,
   8.223 -  classrel: string StringPairTab.table * (class * class) Symtab.table,
   8.224 -  tyco: tyco Symtab.table * tyco Symtab.table,
   8.225 -  instance: string StringPairTab.table * (class * tyco) Symtab.table
   8.226 -}
   8.227 -
   8.228 -val empty_names = Names {
   8.229 -  class = (Symtab.empty, Symtab.empty),
   8.230 -  classrel = (StringPairTab.empty, Symtab.empty),
   8.231 -  tyco = (Symtab.empty, Symtab.empty),
   8.232 -  instance = (StringPairTab.empty, Symtab.empty)
   8.233 -};
   8.234 -
   8.235 -local
   8.236 -  fun mk_names (class, classrel, tyco, instance) =
   8.237 -    Names { class = class, classrel = classrel, tyco = tyco, instance = instance };
   8.238 -  fun map_names f (Names { class, classrel, tyco, instance }) =
   8.239 -    mk_names (f (class, classrel, tyco, instance));
   8.240 -in
   8.241 -  fun merge_names (Names { class = (class1, classrev1),
   8.242 -      classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1),
   8.243 -      instance = (instance1, instancerev1) },
   8.244 -    Names { class = (class2, classrev2),
   8.245 -      classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
   8.246 -      instance = (instance2, instancerev2) }) =
   8.247 -    mk_names ((Symtab.merge (op =) (class1, class2), Symtab.merge (op =) (classrev1, classrev2)),
   8.248 -      (StringPairTab.merge (op =) (classrel1, classrel2), Symtab.merge (op =) (classrelrev1, classrelrev2)),
   8.249 -      (Symtab.merge (op =) (tyco1, tyco2), Symtab.merge (op =) (tycorev1, tycorev2)),
   8.250 -      (StringPairTab.merge (op =) (instance1, instance2), Symtab.merge (op =) (instancerev1, instancerev2)));
   8.251 -  fun map_class f = map_names
   8.252 -    (fn (class, classrel, tyco, inst) => (f class, classrel, tyco, inst));
   8.253 -  fun map_classrel f = map_names
   8.254 -    (fn (class, classrel, tyco, inst) => (class, f classrel, tyco, inst));
   8.255 -  fun map_tyco f = map_names
   8.256 -    (fn (class, classrel, tyco, inst) => (class, classrel, f tyco, inst));
   8.257 -  fun map_instance f = map_names
   8.258 -    (fn (class, classrel, tyco, inst) => (class, classrel, tyco, f inst));
   8.259 -end; (*local*)
   8.260 -
   8.261 -structure Code_Name = TheoryDataFun
   8.262 -(
   8.263 -  type T = names ref;
   8.264 -  val empty = ref empty_names;
   8.265 -  fun copy (ref names) = ref names;
   8.266 -  val extend = copy;
   8.267 -  fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
   8.268 -);
   8.269 -
   8.270 -structure ConstName = CodeDataFun
   8.271 -(
   8.272 -  type T = const Symtab.table * string Symtab.table;
   8.273 -  val empty = (Symtab.empty, Symtab.empty);
   8.274 -  fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const,
   8.275 -    fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
   8.276 -);
   8.277 -
   8.278 -val setup = Code_Name.init;
   8.279 -
   8.280 -
   8.281 -(* forward lookup with cache update *)
   8.282 -
   8.283 -fun get thy get_tabs get upd_names upd policy x =
   8.284 -  let
   8.285 -    val names_ref = Code_Name.get thy;
   8.286 -    val (Names names) = ! names_ref;
   8.287 -    val tabs = get_tabs names;
   8.288 -    fun declare name =
   8.289 -      let
   8.290 -        val names' = upd_names (K (upd (x, name) (fst tabs),
   8.291 -          Symtab.update_new (name, x) (snd tabs))) (Names names)
   8.292 -      in (names_ref := names'; name) end;
   8.293 -  in case get (fst tabs) x
   8.294 -   of SOME name => name
   8.295 -    | NONE => 
   8.296 -        x
   8.297 -        |> policy thy
   8.298 -        |> Name.variant (Symtab.keys (snd tabs))
   8.299 -        |> declare
   8.300 -  end;
   8.301 -
   8.302 -fun get_const thy const =
   8.303 -  let
   8.304 -    val tabs = ConstName.get thy;
   8.305 -    fun declare name =
   8.306 -      let
   8.307 -        val names' = (Symtab.update (const, name) (fst tabs),
   8.308 -          Symtab.update_new (name, const) (snd tabs))
   8.309 -      in (ConstName.change thy (K names'); name) end;
   8.310 -  in case Symtab.lookup (fst tabs) const
   8.311 -   of SOME name => name
   8.312 -    | NONE => 
   8.313 -        const
   8.314 -        |> const_policy thy
   8.315 -        |> Name.variant (Symtab.keys (snd tabs))
   8.316 -        |> declare
   8.317 +    val mns = NameSpace.explode mn;
   8.318 +    val mns' = map (purify_name true false) mns;
   8.319 +  in
   8.320 +    if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
   8.321 +      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
   8.322    end;
   8.323  
   8.324  
   8.325 -(* backward lookup *)
   8.326 +(** variable name contexts **)
   8.327 +
   8.328 +type var_ctxt = string Symtab.table * Name.context;
   8.329  
   8.330 -fun rev thy get_tabs name =
   8.331 +fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
   8.332 +  Name.make_context names);
   8.333 +
   8.334 +fun intro_vars names (namemap, namectxt) =
   8.335    let
   8.336 -    val names_ref = Code_Name.get thy
   8.337 -    val (Names names) = ! names_ref;
   8.338 -    val tab = (snd o get_tabs) names;
   8.339 -  in case Symtab.lookup tab name
   8.340 -   of SOME x => x
   8.341 -    | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name)
   8.342 -  end;
   8.343 +    val (names', namectxt') = Name.variants names namectxt;
   8.344 +    val namemap' = fold2 (curry Symtab.update) names names' namemap;
   8.345 +  in (namemap', namectxt') end;
   8.346  
   8.347 -fun rev_const thy name =
   8.348 -  let
   8.349 -    val tab = snd (ConstName.get thy);
   8.350 -  in case Symtab.lookup tab name
   8.351 -   of SOME const => const
   8.352 -    | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name)
   8.353 -  end;
   8.354 +fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
   8.355 + of SOME name' => name'
   8.356 +  | NONE => error ("Invalid name in context: " ^ quote name);
   8.357  
   8.358  
   8.359 -(* external interfaces *)
   8.360 -
   8.361 -fun class thy =
   8.362 -  get thy #class Symtab.lookup map_class Symtab.update class_policy
   8.363 -  #> add_suffix suffix_class;
   8.364 -fun classrel thy =
   8.365 -  get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
   8.366 -  #> add_suffix suffix_classrel;
   8.367 -fun tyco thy =
   8.368 -  get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
   8.369 -  #> add_suffix suffix_tyco;
   8.370 -fun instance thy =
   8.371 -  get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
   8.372 -  #> add_suffix suffix_instance;
   8.373 -fun const thy =
   8.374 -  get_const thy
   8.375 -  #> add_suffix suffix_const;
   8.376 +(** misc **)
   8.377  
   8.378 -fun class_rev thy =
   8.379 -  dest_suffix suffix_class
   8.380 -  #> Option.map (rev thy #class);
   8.381 -fun classrel_rev thy =
   8.382 -  dest_suffix suffix_classrel
   8.383 -  #> Option.map (rev thy #classrel);
   8.384 -fun tyco_rev thy =
   8.385 -  dest_suffix suffix_tyco
   8.386 -  #> Option.map (rev thy #tyco);
   8.387 -fun instance_rev thy =
   8.388 -  dest_suffix suffix_instance
   8.389 -  #> Option.map (rev thy #instance);
   8.390 -fun const_rev thy =
   8.391 -  dest_suffix suffix_const
   8.392 -  #> Option.map (rev_const thy);
   8.393 -
   8.394 -local
   8.395 +fun read_const_exprs thy =
   8.396 +  let
   8.397 +    fun consts_of some_thyname =
   8.398 +      let
   8.399 +        val thy' = case some_thyname
   8.400 +         of SOME thyname => ThyInfo.the_theory thyname thy
   8.401 +          | NONE => thy;
   8.402 +        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   8.403 +          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
   8.404 +        fun belongs_here c =
   8.405 +          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
   8.406 +      in case some_thyname
   8.407 +       of NONE => cs
   8.408 +        | SOME thyname => filter belongs_here cs
   8.409 +      end;
   8.410 +    fun read_const_expr "*" = ([], consts_of NONE)
   8.411 +      | read_const_expr s = if String.isSuffix ".*" s
   8.412 +          then ([], consts_of (SOME (unsuffix ".*" s)))
   8.413 +          else ([Code_Unit.read_const thy s], []);
   8.414 +  in pairself flat o split_list o map read_const_expr end;
   8.415  
   8.416 -val f_mapping = [
   8.417 -  (suffix_class,       class_rev),
   8.418 -  (suffix_classrel,    Option.map string_of_classrel oo classrel_rev),
   8.419 -  (suffix_tyco,        tyco_rev),
   8.420 -  (suffix_instance,    Option.map string_of_instance oo instance_rev),
   8.421 -  (suffix_const,       fn thy => Option.map (Code_Unit.string_of_const thy) o const_rev thy)
   8.422 -];
   8.423 -
   8.424 -in
   8.425 -
   8.426 -val value_name = "Isabelle_Eval.EVAL.EVAL"
   8.427 -
   8.428 -fun labelled_name thy suffix_name = if suffix_name = value_name then "<term>" else
   8.429 +fun mk_name_module reserved_names module_prefix module_alias program =
   8.430    let
   8.431 -    val category = category_of suffix_name;
   8.432 -    val name = NameSpace.qualifier suffix_name;
   8.433 -    val suffix = NameSpace.base suffix_name
   8.434 -  in case (the o AList.lookup (op =) f_mapping) suffix thy suffix_name
   8.435 -   of SOME thing => category ^ " " ^ quote thing
   8.436 -    | NONE => error ("Unknown name: " ^ quote name)
   8.437 -  end;
   8.438 +    fun mk_alias name = case module_alias name
   8.439 +     of SOME name' => name'
   8.440 +      | NONE => name
   8.441 +          |> NameSpace.explode
   8.442 +          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
   8.443 +          |> NameSpace.implode;
   8.444 +    fun mk_prefix name = case module_prefix
   8.445 +     of SOME module_prefix => NameSpace.append module_prefix name
   8.446 +      | NONE => name;
   8.447 +    val tab =
   8.448 +      Symtab.empty
   8.449 +      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   8.450 +           o fst o dest_name o fst)
   8.451 +             program
   8.452 +  in the o Symtab.lookup tab end;
   8.453  
   8.454  end;
   8.455 -
   8.456 -end;
     9.1 --- a/src/Tools/code/code_printer.ML	Wed Oct 22 14:15:44 2008 +0200
     9.2 +++ b/src/Tools/code/code_printer.ML	Wed Oct 22 14:15:45 2008 +0200
     9.3 @@ -7,15 +7,7 @@
     9.4  
     9.5  signature CODE_PRINTER =
     9.6  sig
     9.7 -  val first_upper: string -> string
     9.8 -  val first_lower: string -> string
     9.9 -  val dest_name: string -> string * string
    9.10 -  val mk_name_module: Name.context -> string option -> (string -> string option)
    9.11 -    -> 'a Graph.T -> string -> string
    9.12 -  type var_ctxt;
    9.13 -  val make_vars: string list -> var_ctxt;
    9.14 -  val intro_vars: string list -> var_ctxt -> var_ctxt;
    9.15 -  val lookup_var: var_ctxt -> string -> string;
    9.16 +  val nerror: thm -> string -> 'a
    9.17  
    9.18    val @@ : 'a * 'a -> 'a list
    9.19    val @| : 'a list * 'a -> 'a list
    9.20 @@ -45,19 +37,21 @@
    9.21    type tyco_syntax
    9.22    type const_syntax
    9.23    val parse_infix: ('a -> 'b) -> lrx * int -> string
    9.24 -  -> int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)
    9.25 +    -> int * ((fixity -> 'b -> Pretty.T)
    9.26 +    -> fixity -> 'a list -> Pretty.T)
    9.27    val parse_syntax: ('a -> 'b) -> OuterParse.token list
    9.28 -    -> (int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)) option
    9.29 -         * OuterParse.token list
    9.30 -  val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) -> fixity
    9.31 -    -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
    9.32 -  val gen_pr_app: (thm -> bool -> var_ctxt -> const * iterm list -> Pretty.T list)
    9.33 -    -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
    9.34 -    -> (string -> const_syntax option) -> (string -> bool)
    9.35 -    -> thm -> bool -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    9.36 +    -> (int * ((fixity -> 'b -> Pretty.T)
    9.37 +    -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
    9.38 +  val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
    9.39 +    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
    9.40 +  val gen_pr_app: (thm -> bool -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
    9.41 +    -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    9.42 +    -> (string -> const_syntax option) -> (string -> bool) -> Code_Thingol.naming
    9.43 +    -> thm -> bool -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
    9.44    val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
    9.45 -    -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
    9.46 -    -> thm -> fixity -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
    9.47 +    -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    9.48 +    -> thm -> fixity
    9.49 +    -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
    9.50  
    9.51    type literals
    9.52    val Literals: { literal_char: string -> string, literal_string: string -> string,
    9.53 @@ -68,8 +62,6 @@
    9.54    val literal_numeral: literals -> bool -> int -> string
    9.55    val literal_list: literals -> Pretty.T list -> Pretty.T
    9.56    val infix_cons: literals -> int * string
    9.57 -
    9.58 -  val nerror: thm -> string -> 'a
    9.59  end;
    9.60  
    9.61  structure Code_Printer : CODE_PRINTER =
    9.62 @@ -79,52 +71,6 @@
    9.63  
    9.64  fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
    9.65  
    9.66 -(** names and naming **)
    9.67 -
    9.68 -(* auxiliary *)
    9.69 -
    9.70 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    9.71 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    9.72 -
    9.73 -val dest_name =
    9.74 -  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
    9.75 -
    9.76 -fun mk_name_module reserved_names module_prefix module_alias program =
    9.77 -  let
    9.78 -    fun mk_alias name = case module_alias name
    9.79 -     of SOME name' => name'
    9.80 -      | NONE => name
    9.81 -          |> NameSpace.explode
    9.82 -          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
    9.83 -          |> NameSpace.implode;
    9.84 -    fun mk_prefix name = case module_prefix
    9.85 -     of SOME module_prefix => NameSpace.append module_prefix name
    9.86 -      | NONE => name;
    9.87 -    val tab =
    9.88 -      Symtab.empty
    9.89 -      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
    9.90 -           o fst o dest_name o fst)
    9.91 -             program
    9.92 -  in the o Symtab.lookup tab end;
    9.93 -
    9.94 -(* variable name contexts *)
    9.95 -
    9.96 -type var_ctxt = string Symtab.table * Name.context;
    9.97 -
    9.98 -fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
    9.99 -  Name.make_context names);
   9.100 -
   9.101 -fun intro_vars names (namemap, namectxt) =
   9.102 -  let
   9.103 -    val (names', namectxt') = Name.variants names namectxt;
   9.104 -    val namemap' = fold2 (curry Symtab.update) names names' namemap;
   9.105 -  in (namemap', namectxt') end;
   9.106 -
   9.107 -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
   9.108 - of SOME name' => name'
   9.109 -  | NONE => error ("Invalid name in context: " ^ quote name);
   9.110 -
   9.111 -
   9.112  (** assembling text pieces **)
   9.113  
   9.114  infixr 5 @@;
   9.115 @@ -182,19 +128,13 @@
   9.116  type class_syntax = string * (string -> string option);
   9.117  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   9.118    -> fixity -> itype list -> Pretty.T);
   9.119 -type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
   9.120 -  -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
   9.121 +type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
   9.122 +  -> Code_Thingol.naming -> thm -> bool -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
   9.123  
   9.124  fun simple_const_syntax x = (Option.map o apsnd)
   9.125 -  (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
   9.126 -
   9.127 -(*int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
   9.128 -  -> )
   9.129 +  (fn pretty => fn pr => fn naming => fn thm => fn pat => fn vars => pretty (pr vars)) x;
   9.130  
   9.131 -('a * ('b -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)) option
   9.132 -***           -> ('a * (('d -> 'b) -> 'e -> 'f -> 'd -> 'c)) option*)
   9.133 -
   9.134 -fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
   9.135 +fun gen_pr_app pr_app pr_term syntax_const is_cons naming thm pat
   9.136      vars fxy (app as ((c, (_, tys)), ts)) =
   9.137    case syntax_const c
   9.138     of NONE => if pat andalso not (is_cons c) then
   9.139 @@ -202,7 +142,7 @@
   9.140          else brackify fxy (pr_app thm pat vars app)
   9.141      | SOME (k, pr) =>
   9.142          let
   9.143 -          fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
   9.144 +          fun pr' fxy ts = pr (pr_term thm pat) naming thm pat vars fxy (ts ~~ curry Library.take k tys);
   9.145          in if k = length ts
   9.146            then pr' fxy ts
   9.147          else if k < length ts
   9.148 @@ -216,9 +156,9 @@
   9.149      val vs = case pat
   9.150       of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
   9.151        | NONE => [];
   9.152 -    val vars' = intro_vars (the_list v) vars;
   9.153 -    val vars'' = intro_vars vs vars';
   9.154 -    val v' = Option.map (lookup_var vars') v;
   9.155 +    val vars' = Code_Name.intro_vars (the_list v) vars;
   9.156 +    val vars'' = Code_Name.intro_vars vs vars';
   9.157 +    val v' = Option.map (Code_Name.lookup_var vars') v;
   9.158      val pat' = Option.map (pr_term thm true vars'' fxy) pat;
   9.159    in (pr_bind ((v', pat'), ty), vars'') end;
   9.160  
    10.1 --- a/src/Tools/code/code_target.ML	Wed Oct 22 14:15:44 2008 +0200
    10.2 +++ b/src/Tools/code/code_target.ML	Wed Oct 22 14:15:45 2008 +0200
    10.3 @@ -11,7 +11,8 @@
    10.4  
    10.5    type serializer
    10.6    val add_target: string * (serializer * literals) -> theory -> theory
    10.7 -  val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
    10.8 +  val extend_target: string *
    10.9 +      (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
   10.10      -> theory -> theory
   10.11    val assert_target: theory -> string -> string
   10.12  
   10.13 @@ -24,20 +25,18 @@
   10.14    val code_writeln: Pretty.T -> unit
   10.15    val mk_serialization: string -> ('a -> unit) option
   10.16      -> (Path.T option -> 'a -> unit)
   10.17 -    -> ('a -> string * string list)
   10.18 +    -> ('a -> string * string option list)
   10.19      -> 'a -> serialization
   10.20    val serialize: theory -> string -> string option -> Args.T list
   10.21 -    -> Code_Thingol.program -> string list -> serialization
   10.22 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   10.23    val serialize_custom: theory -> string * (serializer * literals)
   10.24 -    -> Code_Thingol.program -> string list -> string * string list
   10.25 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   10.26    val the_literals: theory -> string -> literals
   10.27    val compile: serialization -> unit
   10.28    val export: serialization -> unit
   10.29    val file: Path.T -> serialization -> unit
   10.30    val string: string list -> serialization -> string
   10.31 -
   10.32    val code_of: theory -> string -> string -> string list -> string list -> string
   10.33 -  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
   10.34    val code_width: int ref
   10.35  
   10.36    val allow_abort: string -> theory -> theory
   10.37 @@ -45,11 +44,7 @@
   10.38      -> (string * (string * string) list) option -> theory -> theory
   10.39    val add_syntax_inst: string -> string * class -> bool -> theory -> theory
   10.40    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
   10.41 -  val add_syntax_tycoP: string -> string -> OuterParse.token list
   10.42 -    -> (theory -> theory) * OuterParse.token list
   10.43    val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
   10.44 -  val add_syntax_constP: string -> string -> OuterParse.token list
   10.45 -    -> (theory -> theory) * OuterParse.token list
   10.46    val add_reserved: string -> string -> theory -> theory
   10.47  end;
   10.48  
   10.49 @@ -62,7 +57,7 @@
   10.50  (** basics **)
   10.51  
   10.52  datatype destination = Compile | Export | File of Path.T | String of string list;
   10.53 -type serialization = destination -> (string * string list) option;
   10.54 +type serialization = destination -> (string * string option list) option;
   10.55  
   10.56  val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
   10.57  fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
   10.58 @@ -87,22 +82,24 @@
   10.59  
   10.60  (** theory data **)
   10.61  
   10.62 +structure StringPairTab = Code_Name.StringPairTab;
   10.63 +
   10.64  datatype name_syntax_table = NameSyntaxTable of {
   10.65    class: class_syntax Symtab.table,
   10.66 -  inst: unit Symtab.table,
   10.67 +  instance: unit StringPairTab.table,
   10.68    tyco: tyco_syntax Symtab.table,
   10.69    const: const_syntax Symtab.table
   10.70  };
   10.71  
   10.72 -fun mk_name_syntax_table ((class, inst), (tyco, const)) =
   10.73 -  NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
   10.74 -fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
   10.75 -  mk_name_syntax_table (f ((class, inst), (tyco, const)));
   10.76 -fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
   10.77 -    NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
   10.78 +fun mk_name_syntax_table ((class, instance), (tyco, const)) =
   10.79 +  NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
   10.80 +fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
   10.81 +  mk_name_syntax_table (f ((class, instance), (tyco, const)));
   10.82 +fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
   10.83 +    NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
   10.84    mk_name_syntax_table (
   10.85      (Symtab.join (K snd) (class1, class2),
   10.86 -       Symtab.join (K snd) (inst1, inst2)),
   10.87 +       StringPairTab.join (K snd) (instance1, instance2)),
   10.88      (Symtab.join (K snd) (tyco1, tyco2),
   10.89         Symtab.join (K snd) (const1, const2))
   10.90    );
   10.91 @@ -117,12 +114,13 @@
   10.92    -> (string -> class_syntax option)
   10.93    -> (string -> tyco_syntax option)
   10.94    -> (string -> const_syntax option)
   10.95 +  -> Code_Thingol.naming
   10.96    -> Code_Thingol.program
   10.97    -> string list                        (*selected statements*)
   10.98    -> serialization;
   10.99  
  10.100  datatype serializer_entry = Serializer of serializer * literals
  10.101 -  | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
  10.102 +  | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
  10.103  
  10.104  datatype target = Target of {
  10.105    serial: serial,
  10.106 @@ -178,19 +176,25 @@
  10.107  
  10.108  fun put_target (target, seri) thy =
  10.109    let
  10.110 -    val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
  10.111 +    val lookup_target = Symtab.lookup (fst (CodeTargetData.get thy));
  10.112      val _ = case seri
  10.113 -     of Extends (super, _) => if defined_target super then ()
  10.114 +     of Extends (super, _) => if is_some (lookup_target super) then ()
  10.115            else error ("Unknown code target language: " ^ quote super)
  10.116        | _ => ();
  10.117 -    val _ = if defined_target target
  10.118 +    val overwriting = case (Option.map the_serializer o lookup_target) target
  10.119 +     of NONE => false
  10.120 +      | SOME (Extends _) => true
  10.121 +      | SOME (Serializer _) => (case seri
  10.122 +         of Extends _ => error ("Will not overwrite existing target " ^ quote target)
  10.123 +          | _ => true);
  10.124 +    val _ = if overwriting
  10.125        then warning ("Overwriting existing target " ^ quote target)
  10.126 -      else ();
  10.127 +      else (); 
  10.128    in
  10.129      thy
  10.130      |> (CodeTargetData.map o apfst oo Symtab.map_default)
  10.131            (target, mk_target ((serial (), seri), (([], Symtab.empty),
  10.132 -            (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
  10.133 +            (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
  10.134                Symtab.empty))))
  10.135            ((map_target o apfst o apsnd o K) seri)
  10.136    end;
  10.137 @@ -241,9 +245,8 @@
  10.138  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  10.139    let
  10.140      val class = prep_class thy raw_class;
  10.141 -    val class' = Code_Name.class thy class;
  10.142      fun mk_classparam c = case AxClass.class_of_param thy c
  10.143 -     of SOME class'' => if class = class'' then Code_Name.const thy c
  10.144 +     of SOME class' => if class = class' then c
  10.145            else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  10.146        | NONE => error ("Not a class operation: " ^ quote c);
  10.147      fun mk_syntax_params raw_params = AList.lookup (op =)
  10.148 @@ -252,30 +255,29 @@
  10.149     of SOME (syntax, raw_params) =>
  10.150        thy
  10.151        |> (map_name_syntax target o apfst o apfst)
  10.152 -           (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
  10.153 +           (Symtab.update (class, (syntax, mk_syntax_params raw_params)))
  10.154      | NONE =>
  10.155        thy
  10.156        |> (map_name_syntax target o apfst o apfst)
  10.157 -           (Symtab.delete_safe class')
  10.158 +           (Symtab.delete_safe class)
  10.159    end;
  10.160  
  10.161  fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  10.162    let
  10.163 -    val inst = Code_Name.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  10.164 +    val inst = (prep_class thy raw_class, prep_tyco thy raw_tyco);
  10.165    in if add_del then
  10.166      thy
  10.167      |> (map_name_syntax target o apfst o apsnd)
  10.168 -        (Symtab.update (inst, ()))
  10.169 +        (StringPairTab.update (inst, ()))
  10.170    else
  10.171      thy
  10.172      |> (map_name_syntax target o apfst o apsnd)
  10.173 -        (Symtab.delete_safe inst)
  10.174 +        (StringPairTab.delete_safe inst)
  10.175    end;
  10.176  
  10.177  fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  10.178    let
  10.179      val tyco = prep_tyco thy raw_tyco;
  10.180 -    val tyco' = if tyco = "fun" then "fun" else Code_Name.tyco thy tyco;
  10.181      fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  10.182        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  10.183        else syntax
  10.184 @@ -283,17 +285,16 @@
  10.185     of SOME syntax =>
  10.186        thy
  10.187        |> (map_name_syntax target o apsnd o apfst)
  10.188 -           (Symtab.update (tyco', check_args syntax))
  10.189 +           (Symtab.update (tyco, check_args syntax))
  10.190     | NONE =>
  10.191        thy
  10.192        |> (map_name_syntax target o apsnd o apfst)
  10.193 -           (Symtab.delete_safe tyco')
  10.194 +           (Symtab.delete_safe tyco)
  10.195    end;
  10.196  
  10.197  fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  10.198    let
  10.199      val c = prep_const thy raw_c;
  10.200 -    val c' = Code_Name.const thy c;
  10.201      fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c
  10.202        then error ("Too many arguments in syntax for constant " ^ quote c)
  10.203        else syntax;
  10.204 @@ -301,11 +302,11 @@
  10.205     of SOME syntax =>
  10.206        thy
  10.207        |> (map_name_syntax target o apsnd o apsnd)
  10.208 -           (Symtab.update (c', check_args syntax))
  10.209 +           (Symtab.update (c, check_args syntax))
  10.210     | NONE =>
  10.211        thy
  10.212        |> (map_name_syntax target o apsnd o apsnd)
  10.213 -           (Symtab.delete_safe c')
  10.214 +           (Symtab.delete_safe c)
  10.215    end;
  10.216  
  10.217  fun add_reserved target =
  10.218 @@ -330,11 +331,10 @@
  10.219  fun add_module_alias target =
  10.220    map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
  10.221  
  10.222 -fun gen_allow_abort prep_cs raw_c thy =
  10.223 +fun gen_allow_abort prep_const raw_c thy =
  10.224    let
  10.225 -    val c = prep_cs thy raw_c;
  10.226 -    val c' = Code_Name.const thy c;
  10.227 -  in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
  10.228 +    val c = prep_const thy raw_c;
  10.229 +  in thy |> (CodeTargetData.map o apsnd) (insert (op =) c) end;
  10.230  
  10.231  fun zip_list (x::xs) f g =
  10.232    f
  10.233 @@ -355,8 +355,6 @@
  10.234  
  10.235  in
  10.236  
  10.237 -val parse_syntax = parse_syntax;
  10.238 -
  10.239  val add_syntax_class = gen_add_syntax_class cert_class (K I);
  10.240  val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  10.241  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  10.242 @@ -370,11 +368,6 @@
  10.243  val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const;
  10.244  val allow_abort_cmd = gen_allow_abort Code_Unit.read_const;
  10.245  
  10.246 -fun add_syntax_tycoP target tyco = parse_syntax I
  10.247 -  >> add_syntax_tyco_cmd target tyco;
  10.248 -fun add_syntax_constP target c = parse_syntax fst
  10.249 -  >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
  10.250 -
  10.251  fun the_literals thy =
  10.252    let
  10.253      val (targets, _) = CodeTargetData.get thy;
  10.254 @@ -390,27 +383,63 @@
  10.255  
  10.256  (* montage *)
  10.257  
  10.258 -fun invoke_serializer thy modify abortable serializer reserved includes 
  10.259 -    module_alias class inst tyco const module args program1 cs1 =
  10.260 +local
  10.261 +
  10.262 +fun labelled_name thy program name = case Graph.get_node program name
  10.263 + of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c)
  10.264 +  | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
  10.265 +  | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c)
  10.266 +  | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
  10.267 +  | Code_Thingol.Classrel (sub, super) => let
  10.268 +        val Code_Thingol.Class (sub, _) = Graph.get_node program sub
  10.269 +        val Code_Thingol.Class (super, _) = Graph.get_node program super
  10.270 +      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
  10.271 +  | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c)
  10.272 +  | Code_Thingol.Classinst ((class, (tyco, _)), _) => let
  10.273 +        val Code_Thingol.Class (class, _) = Graph.get_node program class
  10.274 +        val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
  10.275 +      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
  10.276 +
  10.277 +fun invoke_serializer thy abortable serializer reserved includes 
  10.278 +    module_alias class instance tyco const module args naming program2 names1 =
  10.279    let
  10.280 -    val program2 = modify program1;
  10.281 -    val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
  10.282 -    val cs2 = subtract (op =) hidden cs1;
  10.283 -    val program3 = Graph.subgraph (not o member (op =) hidden) program2;
  10.284 -    val all_cs = Graph.all_succs program2 cs2;
  10.285 -    val program4 = Graph.subgraph (member (op =) all_cs) program3;
  10.286 +    fun distill_names lookup_name src_tab = Symtab.empty
  10.287 +      |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier
  10.288 +           of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
  10.289 +            | NONE => (NONE, tab)) (Symtab.keys src_tab)
  10.290 +      |>> map_filter I;
  10.291 +    fun lookup_classparam_rev c' = case try (Graph.get_node program2) c'
  10.292 +     of SOME (Code_Thingol.Classparam (c, _)) => SOME c
  10.293 +      | NONE => NONE;
  10.294 +    fun lookup_tyco_fun naming "fun" = SOME "fun"
  10.295 +      | lookup_tyco_fun naming tyco = Code_Thingol.lookup_tyco naming tyco;
  10.296 +    val (names_class, class') = distill_names Code_Thingol.lookup_class class;
  10.297 +    val class'' = class'
  10.298 +      |> (Symtab.map o apsnd) (fn class_params => fn c' =>
  10.299 +          case lookup_classparam_rev c'
  10.300 +           of SOME c => class_params c
  10.301 +            | NONE => NONE)
  10.302 +    val names_inst = map_filter (Code_Thingol.lookup_instance naming)
  10.303 +      (StringPairTab.keys instance);
  10.304 +    val (names_tyco, tyco') = distill_names lookup_tyco_fun tyco;
  10.305 +    val (names_const, const') = distill_names Code_Thingol.lookup_const const;
  10.306 +    val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
  10.307 +    val names2 = subtract (op =) names_hidden names1;
  10.308 +    val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
  10.309 +    val names_all = Graph.all_succs program2 names2;
  10.310 +    val program4 = Graph.subgraph (member (op =) names_all) program3;
  10.311      val empty_funs = filter_out (member (op =) abortable)
  10.312        (Code_Thingol.empty_funs program3);
  10.313      val _ = if null empty_funs then () else error ("No defining equations for "
  10.314 -      ^ commas (map (Code_Name.labelled_name thy) empty_funs));
  10.315 +      ^ commas (map (Sign.extern_const thy) empty_funs));
  10.316    in
  10.317 -    serializer module args (Code_Name.labelled_name thy) reserved includes
  10.318 -      (Symtab.lookup module_alias) (Symtab.lookup class)
  10.319 -      (Symtab.lookup tyco) (Symtab.lookup const)
  10.320 -      program4 cs2
  10.321 +    serializer module args (labelled_name thy program2) reserved includes
  10.322 +      (Symtab.lookup module_alias) (Symtab.lookup class'')
  10.323 +      (Symtab.lookup tyco') (Symtab.lookup const')
  10.324 +      naming program4 names2
  10.325    end;
  10.326  
  10.327 -fun mount_serializer thy alt_serializer target =
  10.328 +fun mount_serializer thy alt_serializer target module args naming program =
  10.329    let
  10.330      val (targets, abortable) = CodeTargetData.get thy;
  10.331      fun collapse_hierarchy target =
  10.332 @@ -422,7 +451,7 @@
  10.333         of Serializer _ => (I, data)
  10.334          | Extends (super, modify) => let
  10.335              val (modify', data') = collapse_hierarchy super
  10.336 -          in (modify' #> modify, merge_target false target (data', data)) end
  10.337 +          in (modify' #> modify naming, merge_target false target (data', data)) end
  10.338        end;
  10.339      val (modify, data) = collapse_hierarchy target;
  10.340      val (serializer, _) = the_default (case the_serializer data
  10.341 @@ -430,18 +459,22 @@
  10.342      val reserved = the_reserved data;
  10.343      val includes = Symtab.dest (the_includes data);
  10.344      val module_alias = the_module_alias data;
  10.345 -    val { class, inst, tyco, const } = the_name_syntax data;
  10.346 +    val { class, instance, tyco, const } = the_name_syntax data;
  10.347    in
  10.348 -    invoke_serializer thy modify abortable serializer reserved
  10.349 -      includes module_alias class inst tyco const
  10.350 +    invoke_serializer thy abortable serializer reserved
  10.351 +      includes module_alias class instance tyco const module args naming (modify program)
  10.352    end;
  10.353  
  10.354 +in
  10.355 +
  10.356  fun serialize thy = mount_serializer thy NONE;
  10.357  
  10.358 -fun serialize_custom thy (target_name, seri) program cs =
  10.359 -  mount_serializer thy (SOME seri) target_name NONE [] program cs (String [])
  10.360 +fun serialize_custom thy (target_name, seri) naming program cs =
  10.361 +  mount_serializer thy (SOME seri) target_name NONE [] naming program cs (String [])
  10.362    |> the;
  10.363  
  10.364 +end; (* local *)
  10.365 +
  10.366  fun parse_args f args =
  10.367    case Scan.read OuterLex.stopper f args
  10.368     of SOME x => x
  10.369 @@ -450,40 +483,47 @@
  10.370  
  10.371  (* code presentation *)
  10.372  
  10.373 -fun code_of thy target module_name cs stmt_names =
  10.374 +fun code_of thy target module_name cs names_stmt =
  10.375    let
  10.376 -    val (cs', program) = Code_Thingol.consts_program thy cs;
  10.377 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
  10.378    in
  10.379 -    string stmt_names (serialize thy target (SOME module_name) [] program cs')
  10.380 +    string names_stmt (serialize thy target (SOME module_name) []
  10.381 +      naming program names_cs)
  10.382    end;
  10.383  
  10.384  
  10.385  (* code generation *)
  10.386  
  10.387 +fun transitivly_non_empty_funs thy naming program =
  10.388 +  let
  10.389 +    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
  10.390 +    val names = map_filter (Code_Thingol.lookup_const naming) cs;
  10.391 +  in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
  10.392 +
  10.393  fun read_const_exprs thy cs =
  10.394    let
  10.395      val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
  10.396 -    val (cs3, program) = Code_Thingol.consts_program thy cs2;
  10.397 -    val cs4 = Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy);
  10.398 +    val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
  10.399 +    val names4 = transitivly_non_empty_funs thy naming program;
  10.400      val cs5 = map_filter
  10.401 -      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
  10.402 +      (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
  10.403    in fold (insert (op =)) cs5 cs1 end;
  10.404  
  10.405  fun cached_program thy = 
  10.406    let
  10.407 -    val program = Code_Thingol.cached_program thy;
  10.408 -  in (Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
  10.409 +    val (naming, program) = Code_Thingol.cached_program thy;
  10.410 +  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
  10.411  
  10.412  fun export_code thy cs seris =
  10.413    let
  10.414 -    val (cs', program) = if null cs then cached_program thy
  10.415 +    val (cs', (naming, program)) = if null cs then cached_program thy
  10.416        else Code_Thingol.consts_program thy cs;
  10.417      fun mk_seri_dest dest = case dest
  10.418       of NONE => compile
  10.419        | SOME "-" => export
  10.420        | SOME f => file (Path.explode f)
  10.421      val _ = map (fn (((target, module), dest), args) =>
  10.422 -      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
  10.423 +      (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
  10.424    in () end;
  10.425  
  10.426  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
  10.427 @@ -563,13 +603,6 @@
  10.428    OuterSyntax.command "export_code" "generate executable code for constants"
  10.429      K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  10.430  
  10.431 -fun shell_command thyname cmd = Toplevel.program (fn _ =>
  10.432 -  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd))
  10.433 -    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
  10.434 -   of SOME f => (writeln "Now generating code..."; f (theory thyname))
  10.435 -    | NONE => error ("Bad directive " ^ quote cmd)))
  10.436 -  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  10.437 -
  10.438  end; (*local*)
  10.439  
  10.440  end; (*struct*)
    11.1 --- a/src/Tools/code/code_thingol.ML	Wed Oct 22 14:15:44 2008 +0200
    11.2 +++ b/src/Tools/code/code_thingol.ML	Wed Oct 22 14:15:45 2008 +0200
    11.3 @@ -40,53 +40,59 @@
    11.4  
    11.5  signature CODE_THINGOL =
    11.6  sig
    11.7 -  include BASIC_CODE_THINGOL;
    11.8 -  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
    11.9 -  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
   11.10 -  val unfold_fun: itype -> itype list * itype;
   11.11 -  val unfold_app: iterm -> iterm * iterm list;
   11.12 -  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
   11.13 -  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
   11.14 -  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
   11.15 -  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   11.16 +  include BASIC_CODE_THINGOL
   11.17 +  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   11.18 +  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   11.19 +  val unfold_fun: itype -> itype list * itype
   11.20 +  val unfold_app: iterm -> iterm * iterm list
   11.21 +  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
   11.22 +  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
   11.23 +  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
   11.24 +  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
   11.25    val unfold_const_app: iterm ->
   11.26 -    ((string * (dict list list * itype list)) * iterm list) option;
   11.27 +    ((string * (dict list list * itype list)) * iterm list) option
   11.28    val collapse_let: ((vname * itype) * iterm) * iterm
   11.29 -    -> (iterm * itype) * (iterm * iterm) list;
   11.30 -  val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm;
   11.31 -  val contains_dictvar: iterm -> bool;
   11.32 -  val locally_monomorphic: iterm -> bool;
   11.33 -  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   11.34 -  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   11.35 -  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   11.36 +    -> (iterm * itype) * (iterm * iterm) list
   11.37 +  val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm
   11.38 +  val contains_dictvar: iterm -> bool
   11.39 +  val locally_monomorphic: iterm -> bool
   11.40 +  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
   11.41 +  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
   11.42 +  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
   11.43 +
   11.44 +  type naming
   11.45 +  val lookup_class: naming -> class -> string option
   11.46 +  val lookup_classrel: naming -> class * class -> string option
   11.47 +  val lookup_tyco: naming -> string -> string option
   11.48 +  val lookup_instance: naming -> class * string -> string option
   11.49 +  val lookup_const: naming -> string -> string option
   11.50  
   11.51    datatype stmt =
   11.52        NoStmt
   11.53 -    | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list
   11.54 -    | Datatype of (vname * sort) list * (string * itype list) list
   11.55 -    | Datatypecons of string
   11.56 -    | Class of vname * ((class * string) list * (string * itype) list)
   11.57 +    | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
   11.58 +    | Datatype of string * ((vname * sort) list * (string * itype list) list)
   11.59 +    | Datatypecons of string * string
   11.60 +    | Class of class * (vname * ((class * string) list * (string * itype) list))
   11.61      | Classrel of class * class
   11.62 -    | Classparam of class
   11.63 +    | Classparam of string * class
   11.64      | Classinst of (class * (string * (vname * sort) list))
   11.65            * ((class * (string * (string * dict list list))) list
   11.66 -        * ((string * const) * (thm * bool)) list);
   11.67 -  type program = stmt Graph.T;
   11.68 -  val empty_funs: program -> string list;
   11.69 -  val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm;
   11.70 -  val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt;
   11.71 -  val transitivly_non_empty_funs: program -> string list -> string list;
   11.72 -  val is_cons: program -> string -> bool;
   11.73 -  val contr_classparam_typs: program -> string -> itype option list;
   11.74 +        * ((string * const) * (thm * bool)) list)
   11.75 +  type program = stmt Graph.T
   11.76 +  val empty_funs: program -> string list
   11.77 +  val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   11.78 +  val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   11.79 +  val is_cons: program -> string -> bool
   11.80 +  val contr_classparam_typs: program -> string -> itype option list
   11.81  
   11.82 -  val consts_program: theory -> string list -> string list * program;
   11.83 -  val cached_program: theory -> program;
   11.84 +  val consts_program: theory -> string list -> string list * (naming * program)
   11.85 +  val cached_program: theory -> naming * program
   11.86    val eval_conv: theory
   11.87 -    -> (term -> term * (program -> typscheme * iterm -> string list -> thm))
   11.88 -    -> cterm -> thm;
   11.89 +    -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> thm))
   11.90 +    -> cterm -> thm
   11.91    val eval_term: theory
   11.92 -    -> (term -> term * (program -> typscheme * iterm -> string list -> 'a))
   11.93 -    -> term -> 'a;
   11.94 +    -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> 'a))
   11.95 +    -> term -> 'a
   11.96  end;
   11.97  
   11.98  structure Code_Thingol: CODE_THINGOL =
   11.99 @@ -109,8 +115,6 @@
  11.100  
  11.101  (** language core - types, patterns, expressions **)
  11.102  
  11.103 -(* language representation *)
  11.104 -
  11.105  type vname = string;
  11.106  
  11.107  datatype dict =
  11.108 @@ -252,18 +256,148 @@
  11.109    | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
  11.110  
  11.111  
  11.112 +(** naming policies **)
  11.113 +
  11.114 +(* identifier categories *)
  11.115 +
  11.116 +val suffix_class = "class";
  11.117 +val suffix_classrel = "classrel"
  11.118 +val suffix_tyco = "tyco";
  11.119 +val suffix_instance = "inst";
  11.120 +val suffix_const = "const";
  11.121 +
  11.122 +fun add_suffix nsp NONE = NONE
  11.123 +  | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
  11.124 +
  11.125 +
  11.126 +(* policies *)
  11.127 +
  11.128 +local
  11.129 +  fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
  11.130 +  fun thyname_of_class thy =
  11.131 +    thyname_of thy (ProofContext.query_class (ProofContext.init thy));
  11.132 +  fun thyname_of_tyco thy =
  11.133 +    thyname_of thy (Type.the_tags (Sign.tsig_of thy));
  11.134 +  fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
  11.135 +   of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
  11.136 +    | thyname :: _ => thyname;
  11.137 +  fun thyname_of_const thy c = case Code.get_datatype_of_constr thy c
  11.138 +     of SOME dtco => thyname_of_tyco thy dtco
  11.139 +      | NONE => (case AxClass.class_of_param thy c
  11.140 +         of SOME class => thyname_of_class thy class
  11.141 +          | NONE => (case AxClass.inst_of_param thy c
  11.142 +             of SOME (c, tyco) => thyname_of_instance thy
  11.143 +                  ((the o AxClass.class_of_param thy) c, tyco)
  11.144 +              | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c));
  11.145 +  fun namify thy get_basename get_thyname name =
  11.146 +    let
  11.147 +      val prefix = get_thyname thy name;
  11.148 +      val base = (Code_Name.purify_base true o get_basename) name;
  11.149 +    in NameSpace.append prefix base end;
  11.150 +in
  11.151 +
  11.152 +fun namify_class thy = namify thy NameSpace.base thyname_of_class;
  11.153 +fun namify_classrel thy = namify thy (fn (class1, class2) => 
  11.154 +  NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
  11.155 +  (*order fits nicely with composed projections*)
  11.156 +fun namify_tyco thy = namify thy NameSpace.base thyname_of_tyco;
  11.157 +fun namify_instance thy = namify thy (fn (class, tyco) => 
  11.158 +  NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
  11.159 +fun namify_const thy = namify thy NameSpace.base thyname_of_const;
  11.160 +
  11.161 +end; (* local *)
  11.162 +
  11.163 +
  11.164 +(* naming data with lookup and declare *)
  11.165 +
  11.166 +structure StringPairTab = Code_Name.StringPairTab;
  11.167 +
  11.168 +datatype naming = Naming of {
  11.169 +  class: class Symtab.table * Name.context,
  11.170 +  classrel: string StringPairTab.table * Name.context,
  11.171 +  tyco: string Symtab.table * Name.context,
  11.172 +  instance: string StringPairTab.table * Name.context,
  11.173 +  const: string Symtab.table * Name.context
  11.174 +}
  11.175 +
  11.176 +fun dest_Naming (Naming naming) = naming;
  11.177 +
  11.178 +val empty_naming = Naming {
  11.179 +  class = (Symtab.empty, Name.context),
  11.180 +  classrel = (StringPairTab.empty, Name.context),
  11.181 +  tyco = (Symtab.empty, Name.context),
  11.182 +  instance = (StringPairTab.empty, Name.context),
  11.183 +  const = (Symtab.empty, Name.context)
  11.184 +};
  11.185 +
  11.186 +local
  11.187 +  fun mk_naming (class, classrel, tyco, instance, const) =
  11.188 +    Naming { class = class, classrel = classrel,
  11.189 +      tyco = tyco, instance = instance, const = const };
  11.190 +  fun map_naming f (Naming { class, classrel, tyco, instance, const }) =
  11.191 +    mk_naming (f (class, classrel, tyco, instance, const));
  11.192 +in
  11.193 +  fun map_class f = map_naming
  11.194 +    (fn (class, classrel, tyco, inst, const) =>
  11.195 +      (f class, classrel, tyco, inst, const));
  11.196 +  fun map_classrel f = map_naming
  11.197 +    (fn (class, classrel, tyco, inst, const) =>
  11.198 +      (class, f classrel, tyco, inst, const));
  11.199 +  fun map_tyco f = map_naming
  11.200 +    (fn (class, classrel, tyco, inst, const) =>
  11.201 +      (class, classrel, f tyco, inst, const));
  11.202 +  fun map_instance f = map_naming
  11.203 +    (fn (class, classrel, tyco, inst, const) =>
  11.204 +      (class, classrel, tyco, f inst, const));
  11.205 +  fun map_const f = map_naming
  11.206 +    (fn (class, classrel, tyco, inst, const) =>
  11.207 +      (class, classrel, tyco, inst, f const));
  11.208 +end; (*local*)
  11.209 +
  11.210 +fun add_variant update (thing, name) (tab, used) =
  11.211 +  let
  11.212 +    val (name', used') = yield_singleton Name.variants name used;
  11.213 +    val tab' = update (thing, name') tab;
  11.214 +  in (tab', used') end;
  11.215 +
  11.216 +fun declare thy mapp lookup update namify thing =
  11.217 +  mapp (add_variant update (thing, namify thy thing))
  11.218 +  #> `(fn naming => the (lookup naming thing));
  11.219 +
  11.220 +val lookup_class = add_suffix suffix_class
  11.221 +  oo Symtab.lookup o fst o #class o dest_Naming;
  11.222 +val lookup_classrel = add_suffix suffix_classrel
  11.223 +  oo StringPairTab.lookup o fst o #classrel o dest_Naming;
  11.224 +val lookup_tyco = add_suffix suffix_tyco
  11.225 +  oo Symtab.lookup o fst o #tyco o dest_Naming;
  11.226 +val lookup_instance = add_suffix suffix_instance
  11.227 +  oo StringPairTab.lookup o fst o #instance o dest_Naming;
  11.228 +val lookup_const = add_suffix suffix_const
  11.229 +  oo Symtab.lookup o fst o #const o dest_Naming;
  11.230 +
  11.231 +fun declare_class thy = declare thy map_class
  11.232 +  lookup_class Symtab.update_new namify_class;
  11.233 +fun declare_classrel thy = declare thy map_classrel
  11.234 +  lookup_classrel StringPairTab.update_new namify_classrel;
  11.235 +fun declare_tyco thy = declare thy map_tyco
  11.236 +  lookup_tyco Symtab.update_new namify_tyco;
  11.237 +fun declare_instance thy = declare thy map_instance
  11.238 +  lookup_instance StringPairTab.update_new namify_instance;
  11.239 +fun declare_const thy = declare thy map_const
  11.240 +  lookup_const Symtab.update_new namify_const;
  11.241 +
  11.242  
  11.243  (** statements, abstract programs **)
  11.244  
  11.245  type typscheme = (vname * sort) list * itype;
  11.246  datatype stmt =
  11.247      NoStmt
  11.248 -  | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list
  11.249 -  | Datatype of (vname * sort) list * (string * itype list) list
  11.250 -  | Datatypecons of string
  11.251 -  | Class of vname * ((class * string) list * (string * itype) list)
  11.252 +  | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
  11.253 +  | Datatype of string * ((vname * sort) list * (string * itype list) list)
  11.254 +  | Datatypecons of string * string
  11.255 +  | Class of class * (vname * ((class * string) list * (string * itype) list))
  11.256    | Classrel of class * class
  11.257 -  | Classparam of class
  11.258 +  | Classparam of string * class
  11.259    | Classinst of (class * (string * (vname * sort) list))
  11.260          * ((class * (string * (string * dict list list))) list
  11.261        * ((string * const) * (thm * bool)) list);
  11.262 @@ -271,7 +405,7 @@
  11.263  type program = stmt Graph.T;
  11.264  
  11.265  fun empty_funs program =
  11.266 -  Graph.fold (fn (name, (Fun (_, []), _)) => cons name
  11.267 +  Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c
  11.268                 | _ => I) program [];
  11.269  
  11.270  fun map_terms_bottom_up f (t as IConst _) = f t
  11.271 @@ -285,8 +419,8 @@
  11.272          (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
  11.273  
  11.274  fun map_terms_stmt f NoStmt = NoStmt
  11.275 -  | map_terms_stmt f (Fun (tysm, eqs)) = Fun (tysm, (map o apfst)
  11.276 -      (fn (ts, t) => (map f ts, f t)) eqs)
  11.277 +  | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst)
  11.278 +      (fn (ts, t) => (map f ts, f t)) eqs))
  11.279    | map_terms_stmt f (stmt as Datatype _) = stmt
  11.280    | map_terms_stmt f (stmt as Datatypecons _) = stmt
  11.281    | map_terms_stmt f (stmt as Class _) = stmt
  11.282 @@ -296,19 +430,13 @@
  11.283        Classinst (arity, (superarities, (map o apfst o apsnd) (fn const =>
  11.284          case f (IConst const) of IConst const' => const') classparms));
  11.285  
  11.286 -fun transitivly_non_empty_funs program names_ignored =
  11.287 -  let
  11.288 -    val names_empty = empty_funs program;
  11.289 -    val names_delete = Graph.all_preds program (subtract (op =) names_ignored names_empty)
  11.290 -  in subtract (op =) names_delete (Graph.keys program) end;
  11.291 -
  11.292  fun is_cons program name = case Graph.get_node program name
  11.293   of Datatypecons _ => true
  11.294    | _ => false;
  11.295  
  11.296  fun contr_classparam_typs program name = case Graph.get_node program name
  11.297 - of Classparam class => let
  11.298 -        val Class (_, (_, params)) = Graph.get_node program class;
  11.299 + of Classparam (_, class) => let
  11.300 +        val Class (_, (_, (_, params))) = Graph.get_node program class;
  11.301          val SOME ty = AList.lookup (op =) params name;
  11.302          val (tys, res_ty) = unfold_fun ty;
  11.303          fun no_tyvar (_ `%% tys) = forall no_tyvar tys
  11.304 @@ -322,22 +450,29 @@
  11.305  
  11.306  (** translation kernel **)
  11.307  
  11.308 -fun ensure_stmt stmtgen name (dep, program) =
  11.309 +fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
  11.310    let
  11.311 -    val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
  11.312 -    fun add_stmt false =
  11.313 -          Graph.default_node (name, NoStmt)
  11.314 -          #> add_dep
  11.315 -          #> curry stmtgen (SOME name)
  11.316 -          ##> snd
  11.317 -          #-> (fn stmt => Graph.map_node name (K stmt))
  11.318 -      | add_stmt true =
  11.319 -          add_dep;
  11.320 -  in
  11.321 -    program
  11.322 -    |> add_stmt (can (Graph.get_node program) name)
  11.323 -    |> pair dep
  11.324 -    |> pair name
  11.325 +    fun add_dep name = case dep
  11.326 +     of NONE => I | SOME dep => Graph.add_edge (dep, name);
  11.327 +  in case lookup naming thing
  11.328 +   of SOME name => program
  11.329 +        |> add_dep name
  11.330 +        |> pair naming
  11.331 +        |> pair dep
  11.332 +        |> pair name
  11.333 +    | NONE => let
  11.334 +          val (name, naming') = declare thing naming;
  11.335 +        in
  11.336 +          program
  11.337 +          |> Graph.default_node (name, NoStmt)
  11.338 +          |> add_dep name
  11.339 +          |> pair naming'
  11.340 +          |> curry generate (SOME name)
  11.341 +          ||> snd
  11.342 +          |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
  11.343 +          |> pair dep
  11.344 +          |> pair name
  11.345 +        end
  11.346    end;
  11.347  
  11.348  fun not_wellsorted thy thm ty sort e =
  11.349 @@ -353,22 +488,20 @@
  11.350    let
  11.351      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
  11.352      val cs = #params (AxClass.get_info thy class);
  11.353 -    val class' = Code_Name.class thy class;
  11.354      val stmt_class =
  11.355        fold_map (fn superclass => ensure_class thy algbr funcgr superclass
  11.356          ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
  11.357        ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
  11.358          ##>> exprgen_typ thy algbr funcgr ty) cs
  11.359 -      #>> (fn info => Class (unprefix "'" Name.aT, info))
  11.360 -  in ensure_stmt stmt_class class' end
  11.361 +      #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
  11.362 +  in ensure_stmt lookup_class (declare_class thy) stmt_class class end
  11.363  and ensure_classrel thy algbr funcgr (subclass, superclass) =
  11.364    let
  11.365 -    val classrel' = Code_Name.classrel thy (subclass, superclass);
  11.366      val stmt_classrel =
  11.367        ensure_class thy algbr funcgr subclass
  11.368        ##>> ensure_class thy algbr funcgr superclass
  11.369        #>> Classrel;
  11.370 -  in ensure_stmt stmt_classrel classrel' end
  11.371 +  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
  11.372  and ensure_tyco thy algbr funcgr "fun" =
  11.373        pair "fun"
  11.374    | ensure_tyco thy algbr funcgr tyco =
  11.375 @@ -381,10 +514,9 @@
  11.376              ##>> fold_map (fn (c, tys) =>
  11.377                ensure_const thy algbr funcgr c
  11.378                ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
  11.379 -            #>> Datatype
  11.380 +            #>> (fn info => Datatype (tyco, info))
  11.381            end;
  11.382 -        val tyco' = Code_Name.tyco thy tyco;
  11.383 -      in ensure_stmt stmt_datatype tyco' end
  11.384 +      in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
  11.385  and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
  11.386    fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
  11.387    #>> (fn sort => (unprefix "'" v, sort))
  11.388 @@ -467,38 +599,33 @@
  11.389        ##>> fold_map exprgen_classparam_inst classparams
  11.390        #>> (fn ((((class, tyco), arity), superarities), classparams) =>
  11.391               Classinst ((class, (tyco, arity)), (superarities, classparams)));
  11.392 -    val inst = Code_Name.instance thy (class, tyco);
  11.393 -  in ensure_stmt stmt_inst inst end
  11.394 +  in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
  11.395  and ensure_const thy algbr funcgr c =
  11.396    let
  11.397 -    val c' = Code_Name.const thy c;
  11.398      fun stmt_datatypecons tyco =
  11.399        ensure_tyco thy algbr funcgr tyco
  11.400 -      #>> Datatypecons;
  11.401 +      #>> (fn tyco => Datatypecons (c, tyco));
  11.402      fun stmt_classparam class =
  11.403        ensure_class thy algbr funcgr class
  11.404 -      #>> Classparam;
  11.405 -    fun stmt_fun trns =
  11.406 +      #>> (fn class => Classparam (c, class));
  11.407 +    fun stmt_fun ((vs, raw_ty), raw_thms) =
  11.408        let
  11.409 -        val raw_thms = Code_Funcgr.eqns funcgr c;
  11.410 -        val (vs, raw_ty) = Code_Funcgr.typ funcgr c;
  11.411          val ty = Logic.unvarifyT raw_ty;
  11.412          val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
  11.413            then raw_thms
  11.414            else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
  11.415        in
  11.416 -        trns
  11.417 -        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
  11.418 -        ||>> exprgen_typ thy algbr funcgr ty
  11.419 -        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
  11.420 -        |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
  11.421 +        fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
  11.422 +        ##>> exprgen_typ thy algbr funcgr ty
  11.423 +        ##>> fold_map (exprgen_eq thy algbr funcgr) thms
  11.424 +        #>> (fn info => Fun (c, info))
  11.425        end;
  11.426 -    val stmtgen = case Code.get_datatype_of_constr thy c
  11.427 +    val stmt_const = case Code.get_datatype_of_constr thy c
  11.428       of SOME tyco => stmt_datatypecons tyco
  11.429        | NONE => (case AxClass.class_of_param thy c
  11.430           of SOME class => stmt_classparam class
  11.431 -          | NONE => stmt_fun)
  11.432 -  in ensure_stmt stmtgen c' end
  11.433 +          | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
  11.434 +  in ensure_stmt lookup_const (declare_const thy) stmt_const c end
  11.435  and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
  11.436        exprgen_app thy algbr funcgr thm ((c, ty), [])
  11.437    | exprgen_term thy algbr funcgr thm (Free (v, _)) =
  11.438 @@ -591,9 +718,9 @@
  11.439  
  11.440  structure Program = CodeDataFun
  11.441  (
  11.442 -  type T = program;
  11.443 -  val empty = Graph.empty;
  11.444 -  fun purge thy cs program =
  11.445 +  type T = naming * program;
  11.446 +  val empty = (empty_naming, Graph.empty);
  11.447 +  fun purge thy cs (naming, program) = empty (*FIXME: problem: un-declaration of names
  11.448      let
  11.449        val cs_exisiting =
  11.450          map_filter (Code_Name.const_rev thy) (Graph.keys program);
  11.451 @@ -601,28 +728,25 @@
  11.452            o map (Code_Name.const thy)
  11.453            o filter (member (op =) cs_exisiting)
  11.454          ) cs;
  11.455 -    in Graph.del_nodes dels program end;
  11.456 +    in Graph.del_nodes dels program end;*)
  11.457  );
  11.458  
  11.459  val cached_program = Program.get;
  11.460  
  11.461 -fun transact f program =
  11.462 -  (NONE, program)
  11.463 -  |> f
  11.464 -  |-> (fn x => fn (_, program) => (x, program));
  11.465 -
  11.466 -fun generate thy funcgr f x =
  11.467 -  Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x));
  11.468 +fun generate thy funcgr f name =
  11.469 +  Program.change_yield thy (fn naming_program => (NONE, naming_program)
  11.470 +    |> f thy (Code.operational_algebra thy) funcgr name
  11.471 +    |-> (fn name => fn (_, naming_program) => (name, naming_program)));
  11.472  
  11.473  
  11.474  (* program generation *)
  11.475  
  11.476  fun consts_program thy cs =
  11.477    let
  11.478 -    fun project_consts cs program =
  11.479 +    fun project_consts cs (naming, program) =
  11.480        let
  11.481          val cs_all = Graph.all_succs program cs;
  11.482 -      in (cs, Graph.subgraph (member (op =) cs_all) program) end;
  11.483 +      in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
  11.484      fun generate_consts thy algebra funcgr =
  11.485        fold_map (ensure_const thy algebra funcgr);
  11.486    in
  11.487 @@ -642,18 +766,19 @@
  11.488        fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
  11.489        ##>> exprgen_typ thy algbr funcgr ty
  11.490        ##>> exprgen_term thy algbr funcgr NONE t
  11.491 -      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), (Drule.dummy_thm, true))]));
  11.492 -    fun term_value (dep, program1) =
  11.493 +      #>> (fn ((vs, ty), t) => Fun
  11.494 +        (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
  11.495 +    fun term_value (dep, (naming, program1)) =
  11.496        let
  11.497 -        val Fun ((vs, ty), [(([], t), _)]) =
  11.498 -          Graph.get_node program1 Code_Name.value_name;
  11.499 -        val deps = Graph.imm_succs program1 Code_Name.value_name;
  11.500 -        val program2 = Graph.del_nodes [Code_Name.value_name] program1;
  11.501 +        val Fun (_, ((vs, ty), [(([], t), _)])) =
  11.502 +          Graph.get_node program1 Term.dummy_patternN;
  11.503 +        val deps = Graph.imm_succs program1 Term.dummy_patternN;
  11.504 +        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
  11.505          val deps_all = Graph.all_succs program2 deps;
  11.506          val program3 = Graph.subgraph (member (op =) deps_all) program2;
  11.507 -      in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
  11.508 +      in (((naming, program3), (((vs, ty), t), deps)), (dep, (naming, program2))) end;
  11.509    in
  11.510 -    ensure_stmt stmt_value Code_Name.value_name
  11.511 +    ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
  11.512      #> snd
  11.513      #> term_value
  11.514    end;
  11.515 @@ -662,8 +787,8 @@
  11.516    let
  11.517      fun evaluator'' evaluator''' funcgr t =
  11.518        let
  11.519 -        val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
  11.520 -      in evaluator''' program vs_ty_t deps end;
  11.521 +        val (((naming, program), (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
  11.522 +      in evaluator''' naming program vs_ty_t deps end;
  11.523      fun evaluator' t =
  11.524        let
  11.525          val (t', evaluator''') = evaluator t;
    12.1 --- a/src/Tools/nbe.ML	Wed Oct 22 14:15:44 2008 +0200
    12.2 +++ b/src/Tools/nbe.ML	Wed Oct 22 14:15:45 2008 +0200
    12.3 @@ -288,15 +288,15 @@
    12.4  
    12.5  (* preparing function equations *)
    12.6  
    12.7 -fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) =
    12.8 +fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =
    12.9        []
   12.10 -  | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) =
   12.11 +  | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) =
   12.12        [(const, (vs, map fst eqns))]
   12.13    | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
   12.14        []
   12.15    | eqns_of_stmt (_, Code_Thingol.Datatype _) =
   12.16        []
   12.17 -  | eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) =
   12.18 +  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (superclasses, classops)))) =
   12.19        let
   12.20          val names = map snd superclasses @ map fst classops;
   12.21          val params = Name.invent_list [] "d" (length names);
   12.22 @@ -364,27 +364,28 @@
   12.23  
   12.24  (* reification *)
   12.25  
   12.26 -fun term_of_univ thy idx_tab t =
   12.27 +fun term_of_univ thy program idx_tab t =
   12.28    let
   12.29      fun take_until f [] = []
   12.30        | take_until f (x::xs) = if f x then [] else x :: take_until f xs;
   12.31 -    fun is_dict (Const (idx, _)) =
   12.32 -          let
   12.33 -            val c = the (Inttab.lookup idx_tab idx);
   12.34 -          in
   12.35 -            (is_some o Code_Name.class_rev thy) c
   12.36 -            orelse (is_some o Code_Name.classrel_rev thy) c
   12.37 -            orelse (is_some o Code_Name.instance_rev thy) c
   12.38 -          end
   12.39 +    fun is_dict (Const (idx, _)) = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
   12.40 +         of Code_Thingol.Class _ => true
   12.41 +          | Code_Thingol.Classrel _ => true
   12.42 +          | Code_Thingol.Classinst _ => true
   12.43 +          | _ => false)
   12.44        | is_dict (DFree _) = true
   12.45        | is_dict _ = false;
   12.46 +    fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
   12.47 +         of Code_Thingol.Fun (c, _) => c
   12.48 +          | Code_Thingol.Datatypecons (c, _) => c
   12.49 +          | Code_Thingol.Classparam (c, _) => c);
   12.50      fun of_apps bounds (t, ts) =
   12.51        fold_map (of_univ bounds) ts
   12.52        #>> (fn ts' => list_comb (t, rev ts'))
   12.53      and of_univ bounds (Const (idx, ts)) typidx =
   12.54            let
   12.55              val ts' = take_until is_dict ts;
   12.56 -            val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
   12.57 +            val c = const_of_idx idx;
   12.58              val (_, T) = Code.default_typscheme thy c;
   12.59              val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
   12.60              val typidx' = typidx + maxidx_of_typ T' + 1;
   12.61 @@ -405,7 +406,7 @@
   12.62  (
   12.63    type T = (Univ option * int) Graph.T * (int * string Inttab.table);
   12.64    val empty = (Graph.empty, (0, Inttab.empty));
   12.65 -  fun purge thy cs (gr, (maxidx, idx_tab)) =
   12.66 +  fun purge thy cs (gr, (maxidx, idx_tab)) = empty (*FIXME
   12.67      let
   12.68        val cs_exisiting =
   12.69          map_filter (Code_Name.const_rev thy) (Graph.keys gr);
   12.70 @@ -413,7 +414,7 @@
   12.71            o map (Code_Name.const thy)
   12.72            o filter (member (op =) cs_exisiting)
   12.73          ) cs;
   12.74 -    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
   12.75 +    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end*);
   12.76  );
   12.77  
   12.78  (* compilation, evaluation and reification *)
   12.79 @@ -425,7 +426,7 @@
   12.80    in
   12.81      vs_ty_t
   12.82      |> eval_term ctxt gr deps
   12.83 -    |> term_of_univ thy idx_tab
   12.84 +    |> term_of_univ thy program idx_tab
   12.85    end;
   12.86  
   12.87  (* evaluation with type reconstruction *)
   12.88 @@ -478,13 +479,13 @@
   12.89  fun norm_conv ct =
   12.90    let
   12.91      val thy = Thm.theory_of_cterm ct;
   12.92 -    fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
   12.93 +    fun evaluator' t naming program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
   12.94      fun evaluator t = (add_triv_classes thy t, evaluator' t);
   12.95    in Code_Thingol.eval_conv thy evaluator ct end;
   12.96  
   12.97  fun norm_term thy t =
   12.98    let
   12.99 -    fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
  12.100 +    fun evaluator' t naming program vs_ty_t deps = eval thy t program vs_ty_t deps;
  12.101      fun evaluator t = (add_triv_classes thy t, evaluator' t);
  12.102    in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
  12.103