src/Tools/code/code_target.ML
changeset 24381 560e8ecdf633
parent 24294 edfe16773fd4
child 24423 ae9cd0e92423
     1.1 --- a/src/Tools/code/code_target.ML	Tue Aug 21 13:30:36 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Tue Aug 21 13:30:38 2007 +0200
     1.3 @@ -293,7 +293,7 @@
     1.4  (** SML/OCaml serializer **)
     1.5  
     1.6  datatype ml_def =
     1.7 -    MLFuns of (string * ((iterm list * iterm) list * typscheme)) list
     1.8 +    MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
     1.9    | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
    1.10    | MLClass of string * ((class * string) list * (vname * (string * itype) list))
    1.11    | MLClassinst of string * ((class * (string * (vname * sort) list))
    1.12 @@ -423,13 +423,13 @@
    1.13                  fun mk [] [] = "val"
    1.14                    | mk (_::_) _ = "fun"
    1.15                    | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
    1.16 -                fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)
    1.17 -                  | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =
    1.18 +                fun chk (_, ((vs, _), (ts, _) :: _)) NONE = SOME (mk ts vs)
    1.19 +                  | chk (_, ((vs, _), (ts, _) :: _)) (SOME defi) =
    1.20                        if defi = mk ts vs then SOME defi
    1.21                        else error ("Mixing simultaneous vals and funs not implemented: "
    1.22                          ^ commas (map (labelled_name o fst) funns));
    1.23                in the (fold chk funns NONE) end;
    1.24 -            fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
    1.25 +            fun pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) =
    1.26                let
    1.27                  val vs = filter_out (null o snd) raw_vs;
    1.28                  val shift = if null eqs' then I else
    1.29 @@ -758,7 +758,7 @@
    1.30                        :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
    1.31                      )
    1.32                    end;
    1.33 -            fun pr_funn definer (name, (eqs, (vs, ty))) =
    1.34 +            fun pr_funn definer (name, ((vs, ty), eqs)) =
    1.35                concat (
    1.36                  str definer
    1.37                  :: (str o deresolv) name
    1.38 @@ -1173,7 +1173,7 @@
    1.39              ) (map pr bs)
    1.40            end
    1.41        | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
    1.42 -    fun pr_def (name, CodeThingol.Fun (eqs, (vs, ty))) =
    1.43 +    fun pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
    1.44            let
    1.45              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
    1.46              fun pr_eq (ts, t) =