added OCaml code generation (without dictionaries)
authorhaftmann
Wed Dec 27 19:10:00 2006 +0100 (2006-12-27)
changeset 21911e29bcab0c81c
parent 21910 5b553ed23251
child 21912 ff45788e7bf9
added OCaml code generation (without dictionaries)
src/HOL/Divides.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/List.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/ROOT.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 27 19:09:59 2006 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Dec 27 19:10:00 2006 +0100
     1.3 @@ -929,6 +929,9 @@
     1.4  code_modulename SML
     1.5    Divides Integer
     1.6  
     1.7 +code_modulename OCaml
     1.8 +  Divides Integer
     1.9 +
    1.10  hide (open) const divmod
    1.11  
    1.12  
     2.1 --- a/src/HOL/Integ/IntArith.thy	Wed Dec 27 19:09:59 2006 +0100
     2.2 +++ b/src/HOL/Integ/IntArith.thy	Wed Dec 27 19:10:00 2006 +0100
     2.3 @@ -361,6 +361,9 @@
     2.4  code_modulename SML
     2.5    Numeral Integer
     2.6  
     2.7 +code_modulename OCaml
     2.8 +  Numeral Integer
     2.9 +
    2.10  lemma Numeral_Pls_refl [code func]:
    2.11    "Numeral.Pls = Numeral.Pls" ..
    2.12  
    2.13 @@ -396,9 +399,11 @@
    2.14  
    2.15  code_type bit
    2.16    (SML "bool")
    2.17 +  (OCaml "bool")
    2.18    (Haskell "Bool")
    2.19  code_const "Numeral.bit.B0" and "Numeral.bit.B1"
    2.20    (SML "false" and "true")
    2.21 +  (OCaml "false" and "true")
    2.22    (Haskell "False" and "True")
    2.23  
    2.24  code_const "number_of \<Colon> int \<Rightarrow> int"
    2.25 @@ -407,12 +412,18 @@
    2.26    (SML "_"
    2.27       and "0/ :/ IntInf.int"
    2.28       and "~1/ :/ IntInf.int"
    2.29 -     and "(_; _; raise Fail \"BIT\")"
    2.30 +     and "!(_; _; raise Fail \"BIT\")"
    2.31       and "IntInf.+/ (_,/ 1)"
    2.32       and "IntInf.-/ (_,/ 1))")
    2.33 +  (OCaml "_"
    2.34 +     and "Big'_int.big'_int'_of'_int/ 0"
    2.35 +     and "Big'_int.big'_int'_of'_int/ -1"
    2.36 +     and "!(_; _; failwith \"BIT\")"
    2.37 +     and "Big'_int.succ'_big'_int"
    2.38 +     and "Big'_int.pred'_big'_int")
    2.39    (Haskell "_"
    2.40       and "0"
    2.41 -     and "negate/ 1"
    2.42 +     and "!(-1)"
    2.43       and "error/ \"BIT\""
    2.44       and "(+)/ 1"
    2.45       and "(-)/ _/ 1")
     3.1 --- a/src/HOL/Integ/IntDef.thy	Wed Dec 27 19:09:59 2006 +0100
     3.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Dec 27 19:10:00 2006 +0100
     3.3 @@ -912,6 +912,7 @@
     3.4  
     3.5  code_type int
     3.6    (SML "IntInf.int")
     3.7 +  (OCaml "Big'_int.big'_int")
     3.8    (Haskell "Integer")
     3.9  
    3.10  code_instance int :: eq
    3.11 @@ -919,34 +920,41 @@
    3.12  
    3.13  code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    3.14    (SML "!((_ : IntInf.int) = _)")
    3.15 +  (OCaml "Big'_int.eq'_big'_int")
    3.16    (Haskell infixl 4 "==")
    3.17  
    3.18  code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    3.19    (SML "IntInf.<= (_, _)")
    3.20 +  (OCaml "Big'_int.le'_big'_int")
    3.21    (Haskell infix 4 "<=")
    3.22  
    3.23  code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    3.24    (SML "IntInf.< (_, _)")
    3.25 +  (OCaml "Big'_int.lt'_big'_int")
    3.26    (Haskell infix 4 "<")
    3.27  
    3.28  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    3.29    (SML "IntInf.+ (_, _)")
    3.30 +  (OCaml "Big'_int.add'_big'_int")
    3.31    (Haskell infixl 6 "+")
    3.32  
    3.33  code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    3.34    (SML "IntInf.- (_, _)")
    3.35 +  (OCaml "Big'_int.sub'_big'_int")
    3.36    (Haskell infixl 6 "-")
    3.37  
    3.38  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    3.39    (SML "IntInf.* (_, _)")
    3.40 +  (OCaml "Big'_int.mult'_big'_int")
    3.41    (Haskell infixl 7 "*")
    3.42  
    3.43  code_const "uminus \<Colon> int \<Rightarrow> int"
    3.44    (SML "IntInf.~")
    3.45 +  (OCaml "Big'_int.minus'_big'_int")
    3.46    (Haskell "negate")
    3.47  
    3.48  code_reserved SML IntInf
    3.49 -code_reserved Haskell Integer negate
    3.50 +code_reserved OCaml Big_int
    3.51  
    3.52  code_modulename SML
    3.53    IntDef Integer
     4.1 --- a/src/HOL/Library/Char_ord.thy	Wed Dec 27 19:09:59 2006 +0100
     4.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Dec 27 19:10:00 2006 +0100
     4.3 @@ -98,6 +98,7 @@
     4.4  
     4.5  code_const char_to_int_pair
     4.6    (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
     4.7 +  (OCaml "failwith \"char'_to'_int'_pair\"")
     4.8    (Haskell "error/ \"char'_to'_int'_pair\"")
     4.9  
    4.10  end
     5.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Dec 27 19:09:59 2006 +0100
     5.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Dec 27 19:10:00 2006 +0100
     5.3 @@ -127,10 +127,12 @@
     5.4  
     5.5  code_const "0::nat"
     5.6    (SML "!(0 : IntInf.int)")
     5.7 +  (OCaml "Big'_int.big'_int'_of'_int/ 0")
     5.8    (Haskell "0")
     5.9  
    5.10  code_const "Suc"
    5.11    (SML "IntInf.+ ((_), 1)")
    5.12 +  (OCaml "Big_int.succ'_big'_int")
    5.13    (Haskell "!((_) + 1)")
    5.14  
    5.15  setup {*
    5.16 @@ -148,6 +150,7 @@
    5.17  
    5.18  code_type nat
    5.19    (SML "IntInf.int")
    5.20 +  (OCaml "Big'_int.big'_int")
    5.21    (Haskell "Integer")
    5.22  
    5.23  consts_code
    5.24 @@ -174,10 +177,12 @@
    5.25  
    5.26  code_const int
    5.27    (SML "_")
    5.28 +  (OCaml "_")
    5.29    (Haskell "_")
    5.30  
    5.31  code_const nat_of_int
    5.32    (SML "_")
    5.33 +  (OCaml "_")
    5.34    (Haskell "_")
    5.35  
    5.36  
    5.37 @@ -220,7 +225,7 @@
    5.38      val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
    5.39      val vname = Name.variant (map fst
    5.40        (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
    5.41 -    val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
    5.42 +    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    5.43      fun lhs_of th = snd (Thm.dest_comb
    5.44        (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    5.45      fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
    5.46 @@ -336,4 +341,8 @@
    5.47    Nat Integer
    5.48    EfficientNat Integer
    5.49  
    5.50 +code_modulename OCaml
    5.51 +  Nat Integer
    5.52 +  EfficientNat Integer
    5.53 +
    5.54  end
     6.1 --- a/src/HOL/Library/ExecutableRat.thy	Wed Dec 27 19:09:59 2006 +0100
     6.2 +++ b/src/HOL/Library/ExecutableRat.thy	Wed Dec 27 19:10:00 2006 +0100
     6.3 @@ -105,6 +105,9 @@
     6.4  code_modulename SML
     6.5    ExecutableRat Rational
     6.6  
     6.7 +code_modulename OCaml
     6.8 +  ExecutableRat Rational
     6.9 +
    6.10  
    6.11  section {* rat as abstype *}
    6.12  
    6.13 @@ -124,7 +127,8 @@
    6.14    "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
    6.15  
    6.16  code_const div_zero
    6.17 -  (SML "raise/ (Fail/ \"Division by zero\")")
    6.18 +  (SML "raise/ Fail/ \"Division by zero\"")
    6.19 +  (OCaml "failwith \"Division by zero\"")
    6.20    (Haskell "error/ \"Division by zero\"")
    6.21  
    6.22  code_gen
     7.1 --- a/src/HOL/Library/ExecutableSet.thy	Wed Dec 27 19:09:59 2006 +0100
     7.2 +++ b/src/HOL/Library/ExecutableSet.thy	Wed Dec 27 19:10:00 2006 +0100
     7.3 @@ -278,6 +278,10 @@
     7.4    ExecutableSet List
     7.5    Set List
     7.6  
     7.7 +code_modulename OCaml
     7.8 +  ExecutableSet List
     7.9 +  Set List
    7.10 +
    7.11  code_modulename Haskell
    7.12    ExecutableSet List
    7.13    Set List
     8.1 --- a/src/HOL/List.thy	Wed Dec 27 19:09:59 2006 +0100
     8.2 +++ b/src/HOL/List.thy	Wed Dec 27 19:10:00 2006 +0100
     8.3 @@ -2545,23 +2545,41 @@
     8.4  
     8.5  code_type list
     8.6    (SML "_ list")
     8.7 +  (OCaml "_ list")
     8.8    (Haskell "![_]")
     8.9  
    8.10  code_const Nil
    8.11    (SML "[]")
    8.12 +  (OCaml "[]")
    8.13    (Haskell "[]")
    8.14  
    8.15  code_type char
    8.16    (SML "char")
    8.17 +  (OCaml "char")
    8.18    (Haskell "Char")
    8.19  
    8.20  code_const Char and char_rec
    8.21      and char_case and "size \<Colon> char \<Rightarrow> nat"
    8.22 -  (SML "raise/ Fail/ \"Char\""
    8.23 -    and "raise/ Fail/ \"char_rec\"" and "raise/ Fail/ \"char_case\"" and "raise/ Fail/ \"size_char\"")
    8.24    (Haskell "error/ \"Char\""
    8.25      and "error/ \"char_rec\"" and "error/ \"char_case\"" and "error/ \"size_char\"")
    8.26  
    8.27 +setup {*
    8.28 +  fold (uncurry (CodegenSerializer.add_undefined "SML")) [
    8.29 +      ("List.char.Char", "(raise Fail \"Char\")"),
    8.30 +      ("List.char.char_rec", "(raise Fail \"char_rec\")"),
    8.31 +      ("List.char.char_case", "(raise Fail \"char_case\")")
    8.32 +    ]
    8.33 +  #> fold (uncurry (CodegenSerializer.add_undefined "OCaml")) [
    8.34 +      ("List.char.Char", "(failwith \"Char\")"),
    8.35 +      ("List.char.char_rec", "(failwith \"char_rec\")"),
    8.36 +      ("List.char.char_case", "(failwith \"char_case\")")
    8.37 +    ]    
    8.38 +*}
    8.39 +
    8.40 +code_const "size \<Colon> char \<Rightarrow> nat"
    8.41 +  (SML "!(_;/ raise Fail \"size'_char\")")
    8.42 +  (OCaml "!(_;/ failwith \"size'_char\")")
    8.43 +
    8.44  code_instance list :: eq and char :: eq
    8.45    (Haskell - and -)
    8.46  
    8.47 @@ -2570,13 +2588,14 @@
    8.48  
    8.49  code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    8.50    (SML "!((_ : char) = _)")
    8.51 +  (OCaml "!((_ : char) = _)")
    8.52    (Haskell infixl 4 "==")
    8.53  
    8.54  code_reserved SML
    8.55    list char nil
    8.56  
    8.57 -code_reserved Haskell
    8.58 -  Char
    8.59 +code_reserved OCaml
    8.60 +  list char
    8.61  
    8.62  setup {*
    8.63  let
    8.64 @@ -2600,6 +2619,8 @@
    8.65    #> Codegen.add_codegen "char_codegen" char_codegen
    8.66    #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
    8.67         (Pretty.enum "," "[" "]") NONE (7, "::")
    8.68 +  #> CodegenSerializer.add_pretty_list "OCaml" "List.list.Nil" "List.list.Cons"
    8.69 +       (Pretty.enum ";" "[" "]") NONE (6, "::")
    8.70    #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
    8.71         (Pretty.enum "," "[" "]") (SOME (ML_Syntax.print_char, ML_Syntax.print_string)) (5, ":")
    8.72    #> CodegenPackage.add_appconst
     9.1 --- a/src/HOL/ex/Classpackage.thy	Wed Dec 27 19:09:59 2006 +0100
     9.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Dec 27 19:10:00 2006 +0100
     9.3 @@ -328,7 +328,7 @@
     9.4  definition "y2 = Y (1::int) 2 3"
     9.5  
     9.6  code_gen "op \<otimes>" \<one> inv
     9.7 -code_gen X Y (SML #) (Haskell -)
     9.8 -code_gen x1 x2 y2 (SML #) (Haskell -)
     9.9 +code_gen X Y (SML #) (Haskell -) (OCaml -)
    9.10 +code_gen x1 x2 y2 (SML #) (Haskell -) (OCaml -)
    9.11  
    9.12  end
    10.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Dec 27 19:09:59 2006 +0100
    10.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Dec 27 19:10:00 2006 +0100
    10.3 @@ -5,77 +5,14 @@
    10.4  header {* Tests and examples for code generator *}
    10.5  
    10.6  theory Codegenerator
    10.7 -imports
    10.8 -  Main
    10.9 -  "~~/src/HOL/ex/Records"
   10.10 -  AssocList
   10.11 -  Binomial
   10.12 -  Commutative_Ring
   10.13 -  GCD
   10.14 -  List_Prefix
   10.15 -  Nat_Infinity
   10.16 -  NatPair
   10.17 -  Nested_Environment
   10.18 -  Permutation
   10.19 -  Primes
   10.20 -  Product_ord
   10.21 -  SetsAndFunctions
   10.22 -  State_Monad
   10.23 -  While_Combinator
   10.24 -  Word
   10.25 -  (*a lot of stuff to test*)
   10.26 +imports ExecutableContent
   10.27  begin
   10.28  
   10.29 -definition
   10.30 -  n :: nat where
   10.31 -  "n = 42"
   10.32 -
   10.33 -definition
   10.34 -  k :: "int" where
   10.35 -  "k = -42"
   10.36 -
   10.37 -datatype mut1 = Tip | Top mut2
   10.38 -  and mut2 = Tip | Top mut1
   10.39 -
   10.40 -consts
   10.41 -  mut1 :: "mut1 \<Rightarrow> mut1"
   10.42 -  mut2 :: "mut2 \<Rightarrow> mut2"
   10.43 -
   10.44 -primrec
   10.45 -  "mut1 mut1.Tip = mut1.Tip"
   10.46 -  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
   10.47 -  "mut2 mut2.Tip = mut2.Tip"
   10.48 -  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
   10.49 -
   10.50 -definition
   10.51 -  "mystring = ''my home is my castle''"
   10.52 -
   10.53 -text {* nested lets and such *}
   10.54 +code_gen "*" (SML #) (Haskell -)
   10.55  
   10.56 -definition
   10.57 -  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
   10.58 -
   10.59 -definition
   10.60 -  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
   10.61 -
   10.62 -definition
   10.63 -  "case_let x = (let (y, z) = x in case y of () => z)"
   10.64 -
   10.65 -definition
   10.66 -  "base_case f = f list_case"
   10.67 +ML {* set Toplevel.debug *}
   10.68 +code_gen (OCaml "~/projects/codegen/test/OCaml/ROOT.ocaml")
   10.69  
   10.70 -definition
   10.71 -  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
   10.72 -
   10.73 -definition
   10.74 -  "keywords fun datatype x instance funa classa =
   10.75 -    Suc fun + datatype * x mod instance - funa - classa"
   10.76 -
   10.77 -hide (open) const keywords
   10.78 -
   10.79 -definition
   10.80 -  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
   10.81 -
   10.82 -(*code_gen "*" (Haskell -) (SML #)*)
   10.83 +code_gen "*"(OCaml "~/projects/codegen/test/OCaml/ROOT.ocaml")
   10.84  
   10.85  end
   10.86 \ No newline at end of file
    11.1 --- a/src/HOL/ex/ROOT.ML	Wed Dec 27 19:09:59 2006 +0100
    11.2 +++ b/src/HOL/ex/ROOT.ML	Wed Dec 27 19:10:00 2006 +0100
    11.3 @@ -8,10 +8,10 @@
    11.4  no_document use_thy "GCD";
    11.5  
    11.6  no_document time_use_thy "Classpackage";
    11.7 -no_document time_use_thy "Codegenerator";
    11.8  no_document time_use_thy "CodeCollections";
    11.9  no_document time_use_thy "CodeEval";
   11.10  no_document time_use_thy "CodeRandom";
   11.11 +no_document time_use_thy "Codegenerator";
   11.12  
   11.13  time_use_thy "Higher_Order_Logic";
   11.14  time_use_thy "Abstract_NAT";
    12.1 --- a/src/Pure/Tools/codegen_serializer.ML	Wed Dec 27 19:09:59 2006 +0100
    12.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Wed Dec 27 19:10:00 2006 +0100
    12.3 @@ -28,9 +28,8 @@
    12.4    val tyco_has_serialization: theory -> string list -> string -> bool;
    12.5  
    12.6    val eval_verbose: bool ref;
    12.7 -  val eval_term: theory ->
    12.8 -    (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
    12.9 -    -> 'a;
   12.10 +  val eval_term: theory -> CodegenThingol.code
   12.11 +    -> (string * 'a option ref) * CodegenThingol.iterm -> 'a;
   12.12    val sml_code_width: int ref;
   12.13  end;
   12.14  
   12.15 @@ -44,6 +43,11 @@
   12.16  
   12.17  (* basics *)
   12.18  
   12.19 +infixr 5 @@;
   12.20 +infixr 5 @|;
   12.21 +fun x @@ y = [x, y];
   12.22 +fun xs @| y = xs @ [y];
   12.23 +
   12.24  datatype lrx = L | R | X;
   12.25  
   12.26  datatype fixity =
   12.27 @@ -94,6 +98,7 @@
   12.28          end;
   12.29  
   12.30  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   12.31 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
   12.32  
   12.33  
   12.34  (* user-defined syntax *)
   12.35 @@ -155,6 +160,31 @@
   12.36      | NONE => error "bad serializer arguments";
   12.37  
   12.38  
   12.39 +(* module names *)
   12.40 +
   12.41 +val dest_name =
   12.42 +  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
   12.43 +
   12.44 +fun mk_modl_name_tab empty_names prefix module_alias code =
   12.45 +  let
   12.46 +    fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
   12.47 +    fun mk_alias name =
   12.48 +     case module_alias name
   12.49 +      of SOME name' => name'
   12.50 +       | NONE => nsp_map (fn name => (the_single o fst)
   12.51 +            (Name.variants [name] empty_names)) name;
   12.52 +    fun mk_prefix name =
   12.53 +      case prefix
   12.54 +       of SOME prefix => NameSpace.append prefix name
   12.55 +        | NONE => name;
   12.56 +    val tab =
   12.57 +      Symtab.empty
   12.58 +      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   12.59 +           o fst o dest_name o fst)
   12.60 +             code
   12.61 +  in (fn name => (the o Symtab.lookup tab) name) end;
   12.62 +
   12.63 +
   12.64  (* list and string serializer *)
   12.65  
   12.66  fun implode_list c_nil c_cons e =
   12.67 @@ -213,15 +243,6 @@
   12.68    in (2, pretty) end;
   12.69  
   12.70  
   12.71 -(* misc *)
   12.72 -
   12.73 -fun dest_name name =
   12.74 -  let
   12.75 -    val (names, name_base) = (split_last o NameSpace.explode) name;
   12.76 -    val (names_mod, name_shallow) = split_last names;
   12.77 -  in (names_mod, (name_shallow, name_base)) end;
   12.78 -
   12.79 -
   12.80  
   12.81  (** SML serializer **)
   12.82  
   12.83 @@ -233,13 +254,12 @@
   12.84          * ((class * (string * inst list list)) list
   12.85        * (string * iterm) list));
   12.86  
   12.87 -fun pr_sml tyco_syntax const_syntax keyword_vars deresolv ml_def =
   12.88 +fun pr_sml tyco_syntax const_syntax keyword_vars deresolv is_cons ml_def =
   12.89    let
   12.90 -    val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
   12.91      fun dictvar v = 
   12.92        first_upper v ^ "_";
   12.93 -    val label = translate_string (fn "." => "__" | c => c)
   12.94 -      o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
   12.95 +    val label = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
   12.96 +    val mk_classop_name = suffix "_" o snd o dest_name;
   12.97      fun pr_tyvar (v, []) =
   12.98            str "()"
   12.99        | pr_tyvar (v, sort) =
  12.100 @@ -271,9 +291,9 @@
  12.101                  (str o deresolv) inst
  12.102                  :: map (pr_insts BR) iss
  12.103                )
  12.104 -          | pr_inst fxy (Context (classes, (v, i))) =
  12.105 +          | pr_inst fxy (Context ((classes, i), (v, k))) =
  12.106                pr_lookup (map (pr_proj o label) classes
  12.107 -                @ (if i = ~1 then [] else [(pr_proj o string_of_int) (i+1)])
  12.108 +                @ (if k = 1 then [] else [(pr_proj o string_of_int) (i+1)])
  12.109                ) ((str o dictvar) v);
  12.110        in case iys
  12.111         of [] => str "()"
  12.112 @@ -333,7 +353,7 @@
  12.113        | pr_term vars _ (IChar c) =
  12.114            (str o prefix "#" o quote)
  12.115              (let val i = ord c
  12.116 -              in if i < 32
  12.117 +              in if i < 32 orelse i = 34 orelse i = 92
  12.118                  then prefix "\\" (string_of_int i)
  12.119                  else c
  12.120                end)
  12.121 @@ -392,16 +412,10 @@
  12.122        else if k = length ts then
  12.123          [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
  12.124        else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
  12.125 -        (str o deresolv) c :: map (pr_term vars BR) ts
  12.126 +        (str o deresolv) c
  12.127 +          :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
  12.128      and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
  12.129 -      case if is_cons c then [] else (map (pr_insts BR) o filter_out null) iss
  12.130 -       of [] =>
  12.131 -            mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app
  12.132 -        | ps =>
  12.133 -            if (is_none o const_syntax) c then
  12.134 -              brackify fxy ((str o deresolv) c :: (ps @ map (pr_term vars BR) ts))
  12.135 -            else
  12.136 -              error ("Cannot apply user defined serialization for function expecting dictionaries: " ^ quote c)
  12.137 +      mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app;
  12.138      fun pr_def (MLFuns (funns as (funn :: funns'))) =
  12.139            let
  12.140              val definer =
  12.141 @@ -427,7 +441,8 @@
  12.142                          ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  12.143                      val vars = keyword_vars
  12.144                        |> CodegenThingol.intro_vars consts
  12.145 -                      |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
  12.146 +                      |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
  12.147 +                           (insert (op =)) ts []);
  12.148                    in
  12.149                      (Pretty.block o Pretty.breaks) (
  12.150                        [str definer, (str o deresolv) name]
  12.151 @@ -476,7 +491,8 @@
  12.152                ];
  12.153              fun pr_classop (classop, ty) =
  12.154                (Pretty.block o Pretty.breaks) [
  12.155 -                (str o suffix "_" o NameSpace.base) classop, str ":", pr_typ NOBR ty
  12.156 +                (*FIXME?*)
  12.157 +                (str o mk_classop_name) classop, str ":", pr_typ NOBR ty
  12.158                ];
  12.159              fun pr_classop_fun (classop, _) =
  12.160                (Pretty.block o Pretty.breaks) [
  12.161 @@ -484,7 +500,7 @@
  12.162                  (str o deresolv) classop,
  12.163                  Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
  12.164                  str "=",
  12.165 -                str ("#" ^ (suffix "_" o NameSpace.base) classop),
  12.166 +                str ("#" ^ mk_classop_name classop),
  12.167                  str (w ^ ";")
  12.168                ];
  12.169            in
  12.170 @@ -518,7 +534,7 @@
  12.171                    |> CodegenThingol.intro_vars consts;
  12.172                in
  12.173                  (Pretty.block o Pretty.breaks) [
  12.174 -                  (str o suffix "_" o NameSpace.base) classop,
  12.175 +                  (str o mk_classop_name) classop,
  12.176                    str "=",
  12.177                    pr_term vars NOBR t
  12.178                  ]
  12.179 @@ -531,7 +547,8 @@
  12.180                str "=",
  12.181                Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
  12.182                str ":",
  12.183 -              pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
  12.184 +              pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]),
  12.185 +              str ";;"
  12.186              ])
  12.187            end;
  12.188    in pr_def ml_def end;
  12.189 @@ -546,13 +563,9 @@
  12.190      str ("end; (*struct " ^ name ^ "*)")
  12.191    ]);
  12.192  
  12.193 -fun pr_ocaml tyco_syntax const_syntax keyword_vars deresolv ml_def =
  12.194 +fun pr_ocaml tyco_syntax const_syntax keyword_vars deresolv is_cons ml_def =
  12.195    let
  12.196 -    val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
  12.197 -    fun dictvar v = 
  12.198 -      first_upper v ^ "_";
  12.199 -    val label = translate_string (fn "." => "__" | c => c)
  12.200 -      o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
  12.201 +    fun dictvar v = "_" ^ first_upper v;
  12.202      fun pr_tyvar (v, []) =
  12.203            str "()"
  12.204        | pr_tyvar (v, sort) =
  12.205 @@ -572,22 +585,28 @@
  12.206            end;
  12.207      fun pr_insts fxy iys =
  12.208        let
  12.209 -        fun pr_proj s = str ("#" ^ s);
  12.210 +        fun dot p2 p1 = Pretty.block [p1, str ".", str p2];
  12.211 +        fun proj k i p = (brackify BR o map str) [
  12.212 +            "match",
  12.213 +            p,
  12.214 +            "with",
  12.215 +            replicate i "_" |> nth_map k (K "d") |> separate (", ") |> implode,
  12.216 +            "-> d"
  12.217 +          ]
  12.218          fun pr_lookup [] p =
  12.219                p
  12.220            | pr_lookup [p'] p =
  12.221 -              brackify BR [p', p]
  12.222 +              dot p' p
  12.223            | pr_lookup (ps as _ :: _) p =
  12.224 -              brackify BR [Pretty.enum " o" "(" ")" ps, p];
  12.225 +              fold_rev dot ps p;
  12.226          fun pr_inst fxy (Instance (inst, iss)) =
  12.227                brackify fxy (
  12.228                  (str o deresolv) inst
  12.229                  :: map (pr_insts BR) iss
  12.230                )
  12.231 -          | pr_inst fxy (Context (classes, (v, i))) =
  12.232 -              pr_lookup (map (pr_proj o label) classes
  12.233 -                @ (if i = ~1 then [] else [(pr_proj o string_of_int) (i+1)])
  12.234 -              ) ((str o dictvar) v);
  12.235 +          | pr_inst fxy (Context ((classes, k), (v, i))) =
  12.236 +              if i = 1 then pr_lookup (map deresolv classes) ((str o dictvar) v)
  12.237 +              else pr_lookup (map deresolv classes) (proj k i (dictvar v));
  12.238        in case iys
  12.239         of [] => str "()"
  12.240          | [iy] => pr_inst fxy iy
  12.241 @@ -628,7 +647,7 @@
  12.242                    let
  12.243                      val vars' = CodegenThingol.intro_vars [v] vars;
  12.244                    in
  12.245 -                    ((Pretty.block o Pretty.breaks) [str "fun", str (CodegenThingol.lookup_var vars' v), str "=>"], vars')
  12.246 +                    (str (CodegenThingol.lookup_var vars' v), vars')
  12.247                    end
  12.248                | pr ((v, SOME p), _) vars =
  12.249                    let
  12.250 @@ -636,17 +655,26 @@
  12.251                      val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
  12.252                      val vars'' = CodegenThingol.intro_vars vs vars';
  12.253                    in
  12.254 -                    ((Pretty.block o Pretty.breaks) [str "fun", str (CodegenThingol.lookup_var vars' v), str "as",
  12.255 -                      pr_term vars'' NOBR p, str "=>"], vars'')
  12.256 +                    (brackify BR [
  12.257 +                        pr_term vars'' NOBR p,
  12.258 +                        str "as",
  12.259 +                        str (CodegenThingol.lookup_var vars' v)
  12.260 +                    ], vars'')
  12.261                    end;
  12.262              val (ps', vars') = fold_map pr ps vars;
  12.263 -          in brackify BR (ps' @ [pr_term vars' NOBR t']) end
  12.264 +          in brackify BR (
  12.265 +              str "fun"
  12.266 +              :: ps'
  12.267 +              @ str "->"
  12.268 +              @@ pr_term vars' NOBR t'
  12.269 +            )
  12.270 +          end
  12.271        | pr_term vars fxy (INum n) =
  12.272 -          brackify BR [(str o IntInf.toString) n, str ":", str "Big_int.big_int"]
  12.273 +          brackify BR [str "Big_int.big_int_of_int", (str o IntInf.toString) n]
  12.274        | pr_term vars _ (IChar c) =
  12.275 -          (str o prefix "#" o quote)
  12.276 +          (str o enclose "'" "'")
  12.277              (let val i = ord c
  12.278 -              in if i < 32
  12.279 +              in if i < 32 orelse i = 39 orelse i = 92
  12.280                  then prefix "\\" (string_of_int i)
  12.281                  else c
  12.282                end)
  12.283 @@ -658,22 +686,18 @@
  12.284                  val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
  12.285                  val vars' = CodegenThingol.intro_vars vs vars;
  12.286                in
  12.287 -                (Pretty.block [
  12.288 -                  (Pretty.block o Pretty.breaks) [
  12.289 -                    str "val",
  12.290 -                    pr_term vars' NOBR p,
  12.291 -                    str "=",
  12.292 -                    pr_term vars NOBR t''
  12.293 -                  ],
  12.294 -                  str ";"
  12.295 +                ((Pretty.block o Pretty.breaks) [
  12.296 +                  str "let",
  12.297 +                  pr_term vars' NOBR p,
  12.298 +                  str "=",
  12.299 +                  pr_term vars NOBR t'',
  12.300 +                  str "in"
  12.301                  ], vars')
  12.302                end
  12.303              val (binds, vars') = fold_map mk ts vars;
  12.304            in
  12.305 -            Pretty.chunks [
  12.306 -              [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
  12.307 -              [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block
  12.308 -            ] end
  12.309 +            Pretty.chunks (binds @ [pr_term vars' NOBR t'])
  12.310 +          end
  12.311        | pr_term vars fxy (ICase ((td, ty), b::bs)) =
  12.312            let
  12.313              fun pr definer (p, t) =
  12.314 @@ -684,7 +708,7 @@
  12.315                  (Pretty.block o Pretty.breaks) [
  12.316                    str definer,
  12.317                    pr_term vars' NOBR p,
  12.318 -                  str "=>",
  12.319 +                  str "->",
  12.320                    pr_term vars' NOBR t
  12.321                  ]
  12.322                end;
  12.323 @@ -704,36 +728,40 @@
  12.324        else if k = length ts then
  12.325          [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
  12.326        else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
  12.327 -        (str o deresolv) c :: map (pr_term vars BR) ts
  12.328 +        (str o deresolv) c
  12.329 +          :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
  12.330      and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
  12.331 -      case if is_cons c then [] else (map (pr_insts BR) o filter_out null) iss
  12.332 -       of [] =>
  12.333 -            mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app
  12.334 -        | ps =>
  12.335 -            if (is_none o const_syntax) c then
  12.336 -              brackify fxy ((str o deresolv) c :: (ps @ map (pr_term vars BR) ts))
  12.337 -            else
  12.338 -              error ("Cannot apply user defined serialization for function expecting dictionaries: " ^ quote c)
  12.339 -    fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
  12.340 -          funn
  12.341 -      | eta_expand_poly_fun (funn as (_, ([_], ([], _)))) =
  12.342 -          funn
  12.343 -      | eta_expand_poly_fun (funn as (_, ([(_::_, _)], _))) =
  12.344 -          funn
  12.345 -      | eta_expand_poly_fun (funn as (_, ([(_, _ `|-> _)], _))) =
  12.346 -          funn
  12.347 -      | eta_expand_poly_fun (funn as (name, ([([], t)], tysm as (vs, ty)))) =
  12.348 -          if (null o fst o CodegenThingol.unfold_fun) ty
  12.349 -              orelse (not o null o filter_out (null o snd)) vs
  12.350 -            then funn
  12.351 -            else (name, ([([IVar "x"], t `$ IVar "x")], tysm));
  12.352 -    fun pr_def (MLFuns (funns as (funn :: funns'))) =
  12.353 +      mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app;
  12.354 +    fun pr_def (MLFuns (funns as funn :: funns')) =
  12.355            let
  12.356 -            fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
  12.357 +            fun fish_parm _ (w as SOME _) = w
  12.358 +              | fish_parm (IVar v) NONE = SOME v
  12.359 +              | fish_parm _ NONE = NONE;
  12.360 +            fun fillup_parm _ (_, SOME v) = v
  12.361 +              | fillup_parm x (i, NONE) = x ^ string_of_int i;
  12.362 +            fun fish_parms vars eqs =
  12.363 +              let
  12.364 +                val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
  12.365 +                val x = Name.variant (map_filter I raw_fished) "x";
  12.366 +                val fished = map_index (fillup_parm x) raw_fished;
  12.367 +                val vars' = CodegenThingol.intro_vars fished vars;
  12.368 +              in map (CodegenThingol.lookup_var vars') fished end;
  12.369 +            fun pr_eq (ts, t) =
  12.370                let
  12.371 -                val vs = filter_out (null o snd) raw_vs;
  12.372 -                val dummy_args = map_index (fn (i, _) => str ("x" ^ string_of_int i)) (fst eq);
  12.373 -                fun pr_eq definer (ts, t) =
  12.374 +                val consts = map_filter
  12.375 +                  (fn c => if (is_some o const_syntax) c
  12.376 +                    then NONE else (SOME o NameSpace.base o deresolv) c)
  12.377 +                    ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  12.378 +                val vars = keyword_vars
  12.379 +                  |> CodegenThingol.intro_vars consts
  12.380 +                  |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
  12.381 +                      (insert (op =)) ts []);
  12.382 +              in (Pretty.block o Pretty.breaks) [
  12.383 +                (Pretty.block o Pretty.commas) (map (pr_term vars BR) ts),
  12.384 +                str "->",
  12.385 +                pr_term vars NOBR t
  12.386 +              ] end;
  12.387 +            fun pr_eqs [(ts, t)] =
  12.388                    let
  12.389                      val consts = map_filter
  12.390                        (fn c => if (is_some o const_syntax) c
  12.391 @@ -741,27 +769,58 @@
  12.392                          ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  12.393                      val vars = keyword_vars
  12.394                        |> CodegenThingol.intro_vars consts
  12.395 -                      |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
  12.396 +                      |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
  12.397 +                          (insert (op =)) ts []);
  12.398                    in
  12.399 -                    (Pretty.block o Pretty.breaks) [
  12.400 -                      str definer,
  12.401 -                      Pretty.list "(" ")" (map (pr_term vars BR) ts),
  12.402 -                      str "->",
  12.403 -                      pr_term vars NOBR t
  12.404 -                    ]
  12.405 +                    (Pretty.block o Pretty.breaks) (
  12.406 +                      map (pr_term vars BR) ts
  12.407 +                      @ str "="
  12.408 +                      @@ pr_term vars NOBR t
  12.409 +                    )
  12.410                    end
  12.411 -              in
  12.412 -                (Pretty.block o Pretty.breaks) (
  12.413 -                  str "let rec"
  12.414 -                  :: (str o deresolv) name
  12.415 -                  :: (map pr_tyvar vs
  12.416 -                  @ dummy_args
  12.417 -                  @ [str "=", str "match", Pretty.list "(" ")" dummy_args, pr_eq "with" eq]
  12.418 -                  @ map (pr_eq "|") eqs')
  12.419 -                )
  12.420 -              end;
  12.421 +              | pr_eqs (eqs as (eq as ([_], _)) :: eqs') =
  12.422 +                  Pretty.block (
  12.423 +                    str "="
  12.424 +                    :: Pretty.brk 1
  12.425 +                    :: str "function"
  12.426 +                    :: Pretty.brk 1
  12.427 +                    :: pr_eq eq
  12.428 +                    :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
  12.429 +                  )
  12.430 +              | pr_eqs (eqs as eq :: eqs') =
  12.431 +                  let
  12.432 +                    val consts = map_filter
  12.433 +                      (fn c => if (is_some o const_syntax) c
  12.434 +                        then NONE else (SOME o NameSpace.base o deresolv) c)
  12.435 +                        ((fold o CodegenThingol.fold_constnames) (insert (op =)) (map snd eqs) []);
  12.436 +                    val vars = keyword_vars
  12.437 +                      |> CodegenThingol.intro_vars consts;
  12.438 +                    val dummy_parms = (map str o fish_parms vars o map fst) eqs;
  12.439 +                  in
  12.440 +                    Pretty.block (
  12.441 +                      Pretty.breaks dummy_parms
  12.442 +                      @ Pretty.brk 1
  12.443 +                      :: str "="
  12.444 +                      :: Pretty.brk 1
  12.445 +                      :: str "match"
  12.446 +                      :: Pretty.brk 1
  12.447 +                      :: (Pretty.block o Pretty.commas) dummy_parms
  12.448 +                      :: Pretty.brk 1
  12.449 +                      :: str "with"
  12.450 +                      :: Pretty.brk 1
  12.451 +                      :: pr_eq eq
  12.452 +                      :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
  12.453 +                    )
  12.454 +                  end;
  12.455 +            fun pr_funn definer (name, (eqs, (vs, ty))) =
  12.456 +              (Pretty.block o Pretty.breaks) (
  12.457 +                str definer
  12.458 +                :: (str o deresolv) name
  12.459 +                :: map_filter (fn (_, []) => NONE | v => SOME (pr_tyvar v)) vs
  12.460 +                @| pr_eqs eqs
  12.461 +              );
  12.462              val (ps, p) = split_last (pr_funn "let rec" funn :: map (pr_funn "and") funns');
  12.463 -          in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
  12.464 +          in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
  12.465       | pr_def (MLDatas (datas as (data :: datas'))) =
  12.466            let
  12.467              fun pr_co (co, []) =
  12.468 @@ -786,20 +845,19 @@
  12.469              val w = dictvar v;
  12.470              fun pr_superclass class =
  12.471                (Pretty.block o Pretty.breaks o map str) [
  12.472 -                label class, ":", "'" ^ v, deresolv class
  12.473 +                deresolv class, ":", "'" ^ v, deresolv class
  12.474                ];
  12.475              fun pr_classop (classop, ty) =
  12.476                (Pretty.block o Pretty.breaks) [
  12.477 -                (str o suffix "_" o NameSpace.base) classop, str ":", pr_typ NOBR ty
  12.478 +                (str o deresolv) classop, str ":", pr_typ NOBR ty
  12.479                ];
  12.480              fun pr_classop_fun (classop, _) =
  12.481                (Pretty.block o Pretty.breaks) [
  12.482 -                str "fun",
  12.483 +                str "let",
  12.484                  (str o deresolv) classop,
  12.485                  Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
  12.486                  str "=",
  12.487 -                str ("#" ^ (suffix "_" o NameSpace.base) classop),
  12.488 -                str (w ^ ";")
  12.489 +                str (w ^ "." ^ deresolv classop ^ ";;")
  12.490                ];
  12.491            in
  12.492              Pretty.chunks (
  12.493 @@ -807,7 +865,7 @@
  12.494                  str ("type '" ^ v),
  12.495                  (str o deresolv) class,
  12.496                  str "=",
  12.497 -                Pretty.enum "," "{" "};" (
  12.498 +                Pretty.enum ";" "{" "};;" (
  12.499                    map pr_superclass superclasses @ map pr_classop classops
  12.500                  )
  12.501                ]
  12.502 @@ -818,7 +876,7 @@
  12.503            let
  12.504              fun pr_superclass (superclass, superinst_iss) =
  12.505                (Pretty.block o Pretty.breaks) [
  12.506 -                (str o label) superclass,
  12.507 +                (str o deresolv) superclass,
  12.508                  str "=",
  12.509                  pr_insts NOBR [Instance superinst_iss]
  12.510                ];
  12.511 @@ -832,21 +890,23 @@
  12.512                    |> CodegenThingol.intro_vars consts;
  12.513                in
  12.514                  (Pretty.block o Pretty.breaks) [
  12.515 -                  (str o suffix "_" o NameSpace.base) classop,
  12.516 +                  (str o deresolv) classop,
  12.517                    str "=",
  12.518                    pr_term vars NOBR t
  12.519                  ]
  12.520                end;
  12.521            in
  12.522 -            (Pretty.block o Pretty.breaks) ([
  12.523 -              str (if null arity then "val" else "fun"),
  12.524 -              (str o deresolv) inst ] @
  12.525 -              map pr_tyvar arity @ [
  12.526 -              str "=",
  12.527 -              Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
  12.528 -              str ":",
  12.529 -              pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
  12.530 -            ])
  12.531 +            (Pretty.block o Pretty.breaks) (
  12.532 +              str "let"
  12.533 +              :: (str o deresolv) inst
  12.534 +              :: map pr_tyvar arity
  12.535 +              @ str "="
  12.536 +              @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
  12.537 +                Pretty.enum ";" "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
  12.538 +                str ":",
  12.539 +                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
  12.540 +              ]
  12.541 +            )
  12.542            end;
  12.543    in pr_def ml_def end;
  12.544  
  12.545 @@ -865,10 +925,13 @@
  12.546  fun seri_ml pr_def pr_modl output reserved_user module_alias module_prolog
  12.547    (_ : string -> (string * (string -> string option)) option) tyco_syntax const_syntax code =
  12.548    let
  12.549 +    val is_cons = fn node => case CodegenThingol.get_def code node
  12.550 +     of CodegenThingol.Datatypecons _ => true
  12.551 +      | _ => false;
  12.552      datatype node =
  12.553          Def of string * ml_def option
  12.554        | Module of string * ((Name.context * Name.context) * node Graph.T);
  12.555 -    val empty_names = ML_Syntax.reserved |> fold Name.declare ("o" :: reserved_user);
  12.556 +    val empty_names = ML_Syntax.reserved |> fold Name.declare reserved_user;
  12.557      val empty_module = ((empty_names, empty_names), Graph.empty);
  12.558      fun map_node [] f = f
  12.559        | map_node (m::ms) f =
  12.560 @@ -889,16 +952,10 @@
  12.561                    in (x, Module (dmodlname, nsp_nodes')) end)
  12.562            in (x, (nsp, nodes')) end;
  12.563      val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved_names @ reserved_user);
  12.564 -    fun name_modl modl =
  12.565 +    val name_modl = mk_modl_name_tab empty_names NONE module_alias code;
  12.566 +    fun name_def upper name nsp =
  12.567        let
  12.568 -        val modlname = NameSpace.implode modl
  12.569 -      in case module_alias modlname
  12.570 -       of SOME modlname' => NameSpace.explode modlname'
  12.571 -        | NONE => map (fn name => (the_single o fst)
  12.572 -            (Name.variants [name] empty_names)) modl
  12.573 -      end;
  12.574 -    fun name_def upper base nsp =
  12.575 -      let
  12.576 +        val (_, base) = dest_name name;
  12.577          val base' = if upper then first_upper base else base;
  12.578          val ([base''], nsp') = Name.variants [base'] nsp;
  12.579        in (base'', nsp') end;
  12.580 @@ -913,16 +970,16 @@
  12.581      fun mk_funs defs =
  12.582        fold_map
  12.583          (fn (name, CodegenThingol.Fun info) =>
  12.584 -              map_nsp_fun (name_def false (NameSpace.base name)) >> (fn base => (base, (name, info)))
  12.585 +              map_nsp_fun (name_def false name) >> (fn base => (base, (name, info)))
  12.586            | (name, def) => error ("Function block containing illegal def: " ^ quote name)
  12.587          ) defs
  12.588        >> (split_list #> apsnd MLFuns);
  12.589      fun mk_datatype defs =
  12.590        fold_map
  12.591          (fn (name, CodegenThingol.Datatype info) =>
  12.592 -              map_nsp_typ (name_def false (NameSpace.base name)) >> (fn base => (base, SOME (name, info)))
  12.593 +              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
  12.594            | (name, CodegenThingol.Datatypecons _) =>
  12.595 -              map_nsp_fun (name_def true (NameSpace.base name)) >> (fn base => (base, NONE))
  12.596 +              map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
  12.597            | (name, def) => error ("Datatype block containing illegal def: " ^ quote name)
  12.598          ) defs
  12.599        >> (split_list #> apsnd (map_filter I
  12.600 @@ -931,16 +988,16 @@
  12.601      fun mk_class defs =
  12.602        fold_map
  12.603          (fn (name, CodegenThingol.Class info) =>
  12.604 -              map_nsp_typ (name_def false (NameSpace.base name)) >> (fn base => (base, SOME (name, info)))
  12.605 +              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
  12.606            | (name, CodegenThingol.Classop _) =>
  12.607 -              map_nsp_fun (name_def false (NameSpace.base name)) >> (fn base => (base, NONE))
  12.608 +              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
  12.609            | (name, def) => error ("Class block containing illegal def: " ^ quote name)
  12.610          ) defs
  12.611        >> (split_list #> apsnd (map_filter I
  12.612          #> (fn [] => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
  12.613               | [info] => MLClass info)));
  12.614      fun mk_inst [(name, CodegenThingol.Classinst info)] =
  12.615 -      map_nsp_fun (name_def false (NameSpace.base name))
  12.616 +      map_nsp_fun (name_def false name)
  12.617        >> (fn base => ([base], MLClassinst (name, info)));
  12.618      fun add_group mk defs nsp_nodes =
  12.619        let
  12.620 @@ -949,34 +1006,35 @@
  12.621            []
  12.622            |> fold (fold (insert (op =)) o Graph.imm_succs code) names
  12.623            |> subtract (op =) names;
  12.624 -        val (modls, defnames) = (split_list o map dest_name) names;
  12.625 +        val (modls, _) = (split_list o map dest_name) names;
  12.626          val modl = (the_single o distinct (op =)) modls
  12.627            handle Empty =>
  12.628 -            error ("Illegal mutual dependencies: " ^ (commas o map fst) defs);
  12.629 +            error ("Illegal mutual dependencies: " ^ commas names);
  12.630          val modl' = name_modl modl;
  12.631 -        fun add_dep defname name'' =
  12.632 +        val modl_explode = NameSpace.explode modl';
  12.633 +        fun add_dep name name'' =
  12.634            let
  12.635 -            val (modl'', defname'') = (apfst name_modl o dest_name) name'';
  12.636 +            val modl'' = (name_modl o fst o dest_name) name'';
  12.637            in if modl' = modl'' then
  12.638 -            map_node modl'
  12.639 -              (Graph.add_edge (NameSpace.implode (modl @ [fst defname, snd defname]), name''))
  12.640 +            map_node modl_explode
  12.641 +              (Graph.add_edge (name, name''))
  12.642            else let
  12.643 -            val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl', modl'');
  12.644 +            val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl_explode, NameSpace.explode modl'');
  12.645            in
  12.646              map_node common
  12.647                (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
  12.648                  handle Graph.CYCLES _ => error ("Dependency "
  12.649 -                  ^ quote (NameSpace.implode (modl' @ [fst defname, snd defname]))
  12.650 +                  ^ quote name
  12.651                    ^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
  12.652            end end;
  12.653        in
  12.654          nsp_nodes
  12.655 -        |> map_nsp_yield modl' (mk defs)
  12.656 +        |> map_nsp_yield modl_explode (mk defs)
  12.657          |-> (fn (base' :: bases', def') =>
  12.658 -           apsnd (map_node modl' (Graph.new_node (name, (Def (base', SOME def')))
  12.659 +           apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))
  12.660                #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases')))
  12.661 -        |> apsnd (fold (fn defname => fold (add_dep defname) deps) defnames)
  12.662 -        |> apsnd (fold (map_node modl' o Graph.add_edge) (product names names))
  12.663 +        |> apsnd (fold (fn name => fold (add_dep name) deps) names)
  12.664 +        |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))
  12.665        end;
  12.666      fun group_defs [(_, CodegenThingol.Bot)] =
  12.667            I
  12.668 @@ -999,8 +1057,8 @@
  12.669            (rev (Graph.strong_conn code)))
  12.670      fun deresolver prefix name = 
  12.671        let
  12.672 -        val (modl, _) = apsnd (uncurry NameSpace.append) (dest_name name);
  12.673 -        val modl' = name_modl modl;
  12.674 +        val modl = (fst o dest_name) name;
  12.675 +        val modl' = (NameSpace.explode o name_modl) modl;
  12.676          val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
  12.677          val defname' =
  12.678            nodes
  12.679 @@ -1015,7 +1073,7 @@
  12.680      fun pr_node prefix (Def (_, NONE)) =
  12.681            NONE
  12.682        | pr_node prefix (Def (_, SOME def)) =
  12.683 -          SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
  12.684 +          SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) is_cons def)
  12.685        | pr_node prefix (Module (dmodlname, (_, nodes))) =
  12.686            SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
  12.687              @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
  12.688 @@ -1051,14 +1109,13 @@
  12.689  
  12.690  fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv deriving_show def =
  12.691    let
  12.692 -    val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
  12.693      fun class_name class = case class_syntax class
  12.694       of NONE => deresolv class
  12.695        | SOME (class, _) => class;
  12.696      fun classop_name class classop = case class_syntax class
  12.697 -     of NONE => NameSpace.base classop
  12.698 +     of NONE => (snd o dest_name) classop
  12.699        | SOME (_, classop_syntax) => case classop_syntax classop
  12.700 -         of NONE => NameSpace.base classop
  12.701 +         of NONE => (snd o dest_name) classop
  12.702            | SOME classop => classop
  12.703      fun pr_typparms tyvars vs =
  12.704        case maps (fn (v, sort) => map (pair v) sort) vs
  12.705 @@ -1133,7 +1190,7 @@
  12.706        | pr_term vars fxy (IChar c) =
  12.707            (str o enclose "'" "'")
  12.708              (let val i = (Char.ord o the o Char.fromString) c
  12.709 -              in if i < 32
  12.710 +              in if i < 32 orelse i = 39 orelse i = 92
  12.711                  then Library.prefix "\\" (string_of_int i)
  12.712                  else c
  12.713                end)
  12.714 @@ -1192,7 +1249,8 @@
  12.715                      ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  12.716                  val vars = keyword_vars
  12.717                    |> CodegenThingol.intro_vars consts
  12.718 -                  |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
  12.719 +                  |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
  12.720 +                       (insert (op =)) ts []);
  12.721                in
  12.722                  (Pretty.block o Pretty.breaks) (
  12.723                    (str o deresolv_here) name
  12.724 @@ -1300,36 +1358,29 @@
  12.725    let
  12.726      val _ = Option.map File.check destination;
  12.727      val empty_names = Name.make_context (reserved_haskell @ reserved_user);
  12.728 -    fun name_modl modl =
  12.729 -      let
  12.730 -        val modlname = NameSpace.implode modl
  12.731 -      in (modlname, case module_alias modlname
  12.732 -       of SOME modlname' => (case module_prefix
  12.733 -            of NONE => modlname'
  12.734 -             | SOME module_prefix => NameSpace.append module_prefix modlname')
  12.735 -        | NONE => NameSpace.implode (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
  12.736 -            (Name.variants [name] empty_names)) modl)))
  12.737 -      end;
  12.738 -    fun add_def (name, (def, deps)) =
  12.739 +    val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code
  12.740 +    fun add_def (name, (def, deps : string list)) =
  12.741        let
  12.742 -        fun name_def base nsp = nsp |>  Name.variants [base] |>> the_single;
  12.743 -        val (modl, (shallow, base)) = dest_name name;
  12.744 -        fun add_name (nsp as (nsp_fun, nsp_typ)) =
  12.745 +        val (modl, base) = dest_name name;
  12.746 +        fun name_def base = Name.variants [base] #>> the_single;
  12.747 +        fun add_fun upper (nsp_fun, nsp_typ) =
  12.748 +          let
  12.749 +            val (base', nsp_fun') = name_def (if upper then first_upper base else base) nsp_fun
  12.750 +          in (base', (nsp_fun', nsp_typ)) end;
  12.751 +        fun add_typ (nsp_fun, nsp_typ) =
  12.752            let
  12.753 -            val base' = if member (op =)
  12.754 -              [CodegenNames.nsp_class, CodegenNames.nsp_tyco, CodegenNames.nsp_dtco] shallow
  12.755 -              then first_upper base else base;
  12.756 -          in case def
  12.757 -           of CodegenThingol.Bot => (base', nsp)
  12.758 -            | CodegenThingol.Fun _ => let val (base'', nsp_fun') = name_def base' nsp_fun in (base'', (nsp_fun', nsp_typ)) end
  12.759 -            | CodegenThingol.Datatype _ => let val (base'', nsp_typ') = name_def base' nsp_typ in (base'', (nsp_fun, nsp_typ')) end
  12.760 -            | CodegenThingol.Datatypecons _ => let val (base'', nsp_fun') = name_def base' nsp_fun in (base'', (nsp_fun', nsp_typ)) end
  12.761 -            | CodegenThingol.Class _ => let val (base'', nsp_typ') = name_def base' nsp_typ in (base'', (nsp_fun, nsp_typ')) end
  12.762 -            | CodegenThingol.Classop _ => let val (base'', nsp_fun') = name_def base' nsp_fun in (base'', (nsp_fun', nsp_typ)) end
  12.763 -            | CodegenThingol.Classinst _ => (base', nsp)
  12.764 -          end;
  12.765 -        val (modlname, modlname') = name_modl modl;
  12.766 -        val deps' = remove (op =) modlname (map (NameSpace.qualifier o NameSpace.qualifier) deps);
  12.767 +            val (base', nsp_typ') = name_def (first_upper base) nsp_typ
  12.768 +          in (base', (nsp_fun, nsp_typ')) end;
  12.769 +        val add_name =
  12.770 +          case def
  12.771 +           of CodegenThingol.Bot => pair base
  12.772 +            | CodegenThingol.Fun _ => add_fun false
  12.773 +            | CodegenThingol.Datatype _ => add_typ
  12.774 +            | CodegenThingol.Datatypecons _ => add_fun true
  12.775 +            | CodegenThingol.Class _ => add_typ
  12.776 +            | CodegenThingol.Classop _ => add_fun false
  12.777 +            | CodegenThingol.Classinst _ => pair base;
  12.778 +        val modlname' = name_modl modl;
  12.779          fun add_def base' =
  12.780            case def
  12.781             of CodegenThingol.Bot => I
  12.782 @@ -1339,27 +1390,25 @@
  12.783                  cons (name, ((NameSpace.append modlname' base', base'), NONE))
  12.784              | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
  12.785        in
  12.786 -        Symtab.map_default (modlname, (modlname', ([], ([], (empty_names, empty_names)))))
  12.787 -            ((apsnd o apfst) (fold (insert (op =)) deps'))
  12.788 -        #> `(fn code => add_name ((snd o snd o snd o the o Symtab.lookup code) modlname))
  12.789 +        Symtab.map_default (modlname', ([], ([], (empty_names, empty_names))))
  12.790 +              (apfst (fold (insert (op =)) deps))
  12.791 +        #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
  12.792          #-> (fn (base', names) =>
  12.793 -              Symtab.map_entry modlname ((apsnd o apsnd) (fn (defs, _) =>
  12.794 -              (add_def base' defs, names))))
  12.795 +              (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
  12.796 +              (add_def base' defs, names)))
  12.797        end;
  12.798      val code' =
  12.799        fold add_def (AList.make (fn name => (Graph.get_node code name, Graph.imm_succs code name))
  12.800          (Graph.strong_conn code |> flat)) Symtab.empty;
  12.801      val init_vars = CodegenThingol.make_vars (reserved_haskell @ reserved_user);
  12.802      fun deresolv name =
  12.803 -      (fst o fst o the o AList.lookup (op =) ((fst o snd o snd o the
  12.804 -        o Symtab.lookup code') ((NameSpace.qualifier o NameSpace.qualifier) name))) name
  12.805 +      (fst o fst o the o AList.lookup (op =) ((fst o snd o the
  12.806 +        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  12.807          handle Option => "(error \"undefined name " ^ name ^ "\")";
  12.808      fun deresolv_here name =
  12.809 -      (snd o fst o the o AList.lookup (op =) ((fst o snd o snd o the
  12.810 -        o Symtab.lookup code') ((NameSpace.qualifier o NameSpace.qualifier) name))) name
  12.811 +      (snd o fst o the o AList.lookup (op =) ((fst o snd o the
  12.812 +        o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  12.813          handle Option => "(error \"undefined name " ^ name ^ "\")";
  12.814 -    val deresolv_module = fst o the o Symtab.lookup code';
  12.815 -        (*FIXME: chain this into every module name access *)
  12.816      fun deriving_show tyco =
  12.817        let
  12.818          fun deriv _ "fun" = false
  12.819 @@ -1372,8 +1421,8 @@
  12.820                andalso forall (deriv' tycos) tys
  12.821            | deriv' _ (ITyVar _) = true
  12.822        in deriv [] tyco end;
  12.823 -    val seri_def = pr_haskell class_syntax tyco_syntax const_syntax init_vars
  12.824 -      deresolv_here deresolv (if string_classes then deriving_show else K false);
  12.825 +    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax init_vars
  12.826 +      deresolv_here (if qualified then deresolv else deresolv_here) (if string_classes then deriving_show else K false);
  12.827      fun write_module (SOME destination) modlname p =
  12.828            let
  12.829              val filename = case modlname
  12.830 @@ -1384,18 +1433,34 @@
  12.831            in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
  12.832        | write_module NONE _ p =
  12.833            writeln (Pretty.setmp_margin 999999 Pretty.output p ^ "\n");
  12.834 -    fun seri_module (modlname, (modlname', (imports, (defs, _)))) =
  12.835 -      Pretty.chunks (
  12.836 -        str ("module " ^ modlname' ^ " where")
  12.837 -        :: map (str o prefix "import qualified ")
  12.838 -          (imports |> map deresolv_module |> distinct (op =) |> remove (op =) modlname') @ (
  12.839 -        (case module_prolog modlname
  12.840 -         of SOME prolog => [str "", prolog, str ""]
  12.841 -          | NONE => [str ""])
  12.842 -        @ separate (str "") (map_filter
  12.843 -          (fn (name, (_, SOME def)) => SOME (seri_def (name, def))
  12.844 -            | (_, (_, NONE)) => NONE) defs))
  12.845 -      ) |> write_module destination modlname';
  12.846 +    fun seri_module (modlname', (imports, (defs, _))) =
  12.847 +      let
  12.848 +        val imports' =
  12.849 +          imports
  12.850 +          |> map (name_modl o fst o dest_name)
  12.851 +          |> distinct (op =)
  12.852 +          |> remove (op =) modlname';
  12.853 +        val qualified =
  12.854 +          imports
  12.855 +          |> map_filter (try deresolv)
  12.856 +          |> map NameSpace.base
  12.857 +          |> has_duplicates (op =);
  12.858 +        val mk_import = str o (if qualified
  12.859 +          then prefix "import qualified "
  12.860 +          else prefix "import ");
  12.861 +      in
  12.862 +        Pretty.chunks (
  12.863 +          str ("module " ^ modlname' ^ " where")
  12.864 +          :: map mk_import imports'
  12.865 +          @ (
  12.866 +          (case module_prolog modlname'
  12.867 +           of SOME prolog => [str "", prolog, str ""]
  12.868 +            | NONE => [str ""])
  12.869 +          @ separate (str "") (map_filter
  12.870 +            (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
  12.871 +              | (_, (_, NONE)) => NONE) defs))
  12.872 +        ) |> write_module destination modlname'
  12.873 +      end;
  12.874    in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
  12.875  
  12.876  val isar_seri_haskell =
  12.877 @@ -1563,9 +1628,9 @@
  12.878  
  12.879  val eval_verbose = ref false;
  12.880  
  12.881 -fun eval_term thy ((ref_name, reff), t) code =
  12.882 +fun eval_term thy code ((ref_name, reff), t) =
  12.883    let
  12.884 -    val val_name = "eval.VALUE.EVAL";
  12.885 +    val val_name = "eval.EVAL.EVAL";
  12.886      val val_name' = "ROOT.eval.EVAL";
  12.887      val data = (the o Symtab.lookup (CodegenSerializerData.get thy)) "SML"
  12.888      val reserved = the_reserved data;
  12.889 @@ -1867,6 +1932,7 @@
  12.890  val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
  12.891    code_reservedP, code_modulenameP, code_moduleprologP];
  12.892  
  12.893 +(*including serializer defaults*)
  12.894  val _ = Context.add_setup (
  12.895    gen_add_syntax_tyco (K I) "SML" "fun" (SOME (2, fn fxy => fn pr_typ => fn [ty1, ty2] =>
  12.896        (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  12.897 @@ -1886,8 +1952,59 @@
  12.898          str "->",
  12.899          pr_typ (INFX (1, R)) ty2
  12.900        ]))
  12.901 -  #> add_reserved "Haskell" "Show"
  12.902 -  #> add_reserved "Haskell" "Read"
  12.903 +  (*IntInt resp. Big_int are added later when CODE extraction for numerals is set up*)
  12.904 +  #> add_reserved "SML" "o" (*dictionary projections use it already*)
  12.905 +  #> fold (add_reserved "Haskell") [
  12.906 +      "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  12.907 +      "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  12.908 +      "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  12.909 +      "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  12.910 +      "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  12.911 +      "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  12.912 +      "ExitSuccess", "False", "GT", "HeapOverflow",
  12.913 +      "IO", "IOError", "IOException", "IllegalOperation",
  12.914 +      "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  12.915 +      "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  12.916 +      "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  12.917 +      "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  12.918 +      "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  12.919 +      "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  12.920 +      "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  12.921 +      "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  12.922 +      "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  12.923 +      "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  12.924 +      "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  12.925 +      "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  12.926 +      "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  12.927 +      "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  12.928 +      "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  12.929 +      "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  12.930 +      "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  12.931 +      "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  12.932 +      "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  12.933 +      "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  12.934 +      "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  12.935 +      "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  12.936 +      "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  12.937 +      "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  12.938 +      "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  12.939 +      "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  12.940 +      "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  12.941 +      "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  12.942 +      "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  12.943 +      "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  12.944 +      "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  12.945 +      "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  12.946 +      "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  12.947 +      "sequence_", "show", "showChar", "showException", "showField", "showList",
  12.948 +      "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  12.949 +      "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  12.950 +      "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  12.951 +      "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  12.952 +      "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  12.953 +      "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  12.954 +    ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*)
  12.955 +
  12.956  )
  12.957  
  12.958  end; (*local*)
    13.1 --- a/src/Pure/Tools/codegen_thingol.ML	Wed Dec 27 19:09:59 2006 +0100
    13.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Wed Dec 27 19:10:00 2006 +0100
    13.3 @@ -18,7 +18,7 @@
    13.4    type vname = string;
    13.5    datatype inst =
    13.6        Instance of string * inst list list
    13.7 -    | Context of class list * (vname * int);
    13.8 +    | Context of (class list * int) * (vname * int);
    13.9    datatype itype =
   13.10        `%% of string * itype list
   13.11      | ITyVar of vname;
   13.12 @@ -120,7 +120,7 @@
   13.13  
   13.14  datatype inst =
   13.15      Instance of string * inst list list
   13.16 -  | Context of class list * (vname * int);
   13.17 +  | Context of (class list * int) * (vname * int);
   13.18  
   13.19  datatype itype =
   13.20      `%% of string * itype list