src/Tools/code/code_target.ML
changeset 25621 97ebdbdb0299
parent 25538 58e8ba3b792b
child 25771 a81c0ad97133
     1.1 --- a/src/Tools/code/code_target.ML	Thu Dec 13 07:09:08 2007 +0100
     1.2 +++ b/src/Tools/code/code_target.ML	Thu Dec 13 07:09:09 2007 +0100
     1.3 @@ -1130,7 +1130,7 @@
     1.4  in
     1.5  
     1.6  fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name
     1.7 -    init_syms deresolv_here deresolv is_cons deriving_show def =
     1.8 +    init_syms deresolv_here deresolv is_cons contr_classparam_typs deriving_show def =
     1.9    let
    1.10      fun class_name class = case class_syntax class
    1.11       of NONE => deresolv class
    1.12 @@ -1139,17 +1139,17 @@
    1.13       of NONE => deresolv_here classparam
    1.14        | SOME (_, classparam_syntax) => case classparam_syntax classparam
    1.15           of NONE => (snd o dest_name) classparam
    1.16 -          | SOME classparam => classparam
    1.17 -    fun pr_typparms tyvars vs =
    1.18 -      case maps (fn (v, sort) => map (pair v) sort) vs
    1.19 -       of [] => str ""
    1.20 -        | xs => Pretty.block [
    1.21 -            Pretty.enum "," "(" ")" (
    1.22 -              map (fn (v, class) => str
    1.23 -                (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) xs
    1.24 -            ),
    1.25 -            str " => "
    1.26 -          ];
    1.27 +          | SOME classparam => classparam;
    1.28 +    fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    1.29 +     of [] => []
    1.30 +      | classbinds => Pretty.enum "," "(" ")" (
    1.31 +          map (fn (v, class) =>
    1.32 +            str (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) classbinds)
    1.33 +          @@ str " => ";
    1.34 +    fun pr_typforall tyvars vs = case map fst vs
    1.35 +     of [] => []
    1.36 +      | vnames => str "forall " :: Pretty.breaks
    1.37 +          (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    1.38      fun pr_tycoexpr tyvars fxy (tyco, tys) =
    1.39        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
    1.40      and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
    1.41 @@ -1164,66 +1164,78 @@
    1.42                  else pr (pr_typ tyvars) fxy tys)
    1.43        | pr_typ tyvars fxy (ITyVar v) =
    1.44            (str o CodeName.lookup_var tyvars) v;
    1.45 -    fun pr_typscheme_expr tyvars (vs, tycoexpr) =
    1.46 -      Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);
    1.47 +    fun pr_typdecl tyvars (vs, tycoexpr) =
    1.48 +      Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
    1.49      fun pr_typscheme tyvars (vs, ty) =
    1.50 -      Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);
    1.51 -    fun pr_term lhs vars fxy (IConst c) =
    1.52 -          pr_app lhs vars fxy (c, [])
    1.53 -      | pr_term lhs vars fxy (t as (t1 `$ t2)) =
    1.54 +      Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
    1.55 +    fun pr_term tyvars lhs vars fxy (IConst c) =
    1.56 +          pr_app tyvars lhs vars fxy (c, [])
    1.57 +      | pr_term tyvars lhs vars fxy (t as (t1 `$ t2)) =
    1.58            (case CodeThingol.unfold_const_app t
    1.59 -           of SOME app => pr_app lhs vars fxy app
    1.60 +           of SOME app => pr_app tyvars lhs vars fxy app
    1.61              | _ =>
    1.62                  brackify fxy [
    1.63 -                  pr_term lhs vars NOBR t1,
    1.64 -                  pr_term lhs vars BR t2
    1.65 +                  pr_term tyvars lhs vars NOBR t1,
    1.66 +                  pr_term tyvars lhs vars BR t2
    1.67                  ])
    1.68 -      | pr_term lhs vars fxy (IVar v) =
    1.69 +      | pr_term tyvars lhs vars fxy (IVar v) =
    1.70            (str o CodeName.lookup_var vars) v
    1.71 -      | pr_term lhs vars fxy (t as _ `|-> _) =
    1.72 +      | pr_term tyvars lhs vars fxy (t as _ `|-> _) =
    1.73            let
    1.74              val (binds, t') = CodeThingol.unfold_abs t;
    1.75 -            fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
    1.76 +            fun pr ((v, pat), ty) = pr_bind tyvars BR ((SOME v, pat), ty);
    1.77              val (ps, vars') = fold_map pr binds vars;
    1.78 -          in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
    1.79 -      | pr_term lhs vars fxy (ICase (cases as (_, t0))) =
    1.80 +          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end
    1.81 +      | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) =
    1.82            (case CodeThingol.unfold_const_app t0
    1.83             of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.84 -                then pr_case vars fxy cases
    1.85 -                else pr_app lhs vars fxy c_ts
    1.86 -            | NONE => pr_case vars fxy cases)
    1.87 -    and pr_app' lhs vars ((c, _), ts) =
    1.88 -      (str o deresolv) c :: map (pr_term lhs vars BR) ts
    1.89 -    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax
    1.90 +                then pr_case tyvars vars fxy cases
    1.91 +                else pr_app tyvars lhs vars fxy c_ts
    1.92 +            | NONE => pr_case tyvars vars fxy cases)
    1.93 +    and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    1.94 +     of [] => (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts
    1.95 +      | fingerprint => let
    1.96 +          val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
    1.97 +          val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
    1.98 +            (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
    1.99 +          fun pr_term_anno (t, NONE) _ = pr_term tyvars lhs vars BR t
   1.100 +            | pr_term_anno (t, SOME _) ty =
   1.101 +                brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty];
   1.102 +        in
   1.103 +          if needs_annotation then
   1.104 +            (str o deresolv) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
   1.105 +          else (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts
   1.106 +        end
   1.107 +    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) const_syntax
   1.108        labelled_name is_cons lhs vars
   1.109 -    and pr_bind fxy = pr_bind_haskell pr_term fxy
   1.110 -    and pr_case vars fxy (cases as ((_, [_]), _)) =
   1.111 +    and pr_bind tyvars = pr_bind_haskell (pr_term tyvars)
   1.112 +    and pr_case tyvars vars fxy (cases as ((_, [_]), _)) =
   1.113            let
   1.114              val (binds, t) = CodeThingol.unfold_let (ICase cases);
   1.115              fun pr ((pat, ty), t) vars =
   1.116                vars
   1.117 -              |> pr_bind BR ((NONE, SOME pat), ty)
   1.118 -              |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])
   1.119 +              |> pr_bind tyvars BR ((NONE, SOME pat), ty)
   1.120 +              |>> (fn p => semicolon [p, str "=", pr_term tyvars false vars NOBR t])
   1.121              val (ps, vars') = fold_map pr binds vars;
   1.122            in
   1.123              Pretty.block_enclose (
   1.124                str "let {",
   1.125 -              concat [str "}", str "in", pr_term false vars' NOBR t]
   1.126 +              concat [str "}", str "in", pr_term tyvars false vars' NOBR t]
   1.127              ) ps
   1.128            end
   1.129 -      | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
   1.130 +      | pr_case tyvars vars fxy (((td, ty), bs as _ :: _), _) =
   1.131            let
   1.132              fun pr (pat, t) =
   1.133                let
   1.134 -                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
   1.135 -              in semicolon [p, str "->", pr_term false vars' NOBR t] end;
   1.136 +                val (p, vars') = pr_bind tyvars NOBR ((NONE, SOME pat), ty) vars;
   1.137 +              in semicolon [p, str "->", pr_term tyvars false vars' NOBR t] end;
   1.138            in
   1.139              Pretty.block_enclose (
   1.140 -              concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],
   1.141 +              concat [str "(case", pr_term tyvars false vars NOBR td, str "of", str "{"],
   1.142                str "})"
   1.143              ) (map pr bs)
   1.144            end
   1.145 -      | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
   1.146 +      | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\"";
   1.147      fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) =
   1.148            let
   1.149              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
   1.150 @@ -1262,9 +1274,9 @@
   1.151                in
   1.152                  semicolon (
   1.153                    (str o deresolv_here) name
   1.154 -                  :: map (pr_term true vars BR) ts
   1.155 +                  :: map (pr_term tyvars true vars BR) ts
   1.156                    @ str "="
   1.157 -                  @@ pr_term false vars NOBR t
   1.158 +                  @@ pr_term tyvars false vars NOBR t
   1.159                  )
   1.160                end;
   1.161            in
   1.162 @@ -1284,7 +1296,7 @@
   1.163            in
   1.164              semicolon [
   1.165                str "data",
   1.166 -              pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
   1.167 +              pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
   1.168              ]
   1.169            end
   1.170        | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
   1.171 @@ -1293,7 +1305,7 @@
   1.172            in
   1.173              semicolon (
   1.174                str "newtype"
   1.175 -              :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
   1.176 +              :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
   1.177                :: str "="
   1.178                :: (str o deresolv_here) co
   1.179                :: pr_typ tyvars BR ty
   1.180 @@ -1311,7 +1323,7 @@
   1.181            in
   1.182              semicolon (
   1.183                str "data"
   1.184 -              :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
   1.185 +              :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
   1.186                :: str "="
   1.187                :: pr_co co
   1.188                :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
   1.189 @@ -1331,7 +1343,7 @@
   1.190              Pretty.block_enclose (
   1.191                Pretty.block [
   1.192                  str "class ",
   1.193 -                pr_typparms tyvars [(v, map fst superclasses)],
   1.194 +                Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
   1.195                  str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
   1.196                  str " where {"
   1.197                ],
   1.198 @@ -1345,13 +1357,13 @@
   1.199                semicolon [
   1.200                  (str o classparam_name class) classparam,
   1.201                  str "=",
   1.202 -                pr_app false init_syms NOBR (c_inst, [])
   1.203 +                pr_app tyvars false init_syms NOBR (c_inst, [])
   1.204                ];
   1.205            in
   1.206              Pretty.block_enclose (
   1.207                Pretty.block [
   1.208                  str "instance ",
   1.209 -                pr_typparms tyvars vs,
   1.210 +                Pretty.block (pr_typcontext tyvars vs),
   1.211                  str (class_name class ^ " "),
   1.212                  pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
   1.213                  str " where {"
   1.214 @@ -1388,6 +1400,7 @@
   1.215    let
   1.216      val _ = Option.map File.check destination;
   1.217      val is_cons = CodeThingol.is_cons code;
   1.218 +    val contr_classparam_typs = CodeThingol.contr_classparam_typs code;
   1.219      val module_alias = if is_some module then K module else raw_module_alias;
   1.220      val init_names = Name.make_context reserved_syms;
   1.221      val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
   1.222 @@ -1460,6 +1473,7 @@
   1.223      fun seri_def qualified = pr_haskell class_syntax tyco_syntax
   1.224        const_syntax labelled_name init_syms
   1.225        deresolv_here (if qualified then deresolv else deresolv_here) is_cons
   1.226 +      contr_classparam_typs
   1.227        (if string_classes then deriving_show else K false);
   1.228      fun write_modulefile (SOME destination) modlname =
   1.229            let
   1.230 @@ -1541,7 +1555,7 @@
   1.231            ])
   1.232        | pr_fun _ = NONE
   1.233      val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names
   1.234 -      I I (K false) (K false);
   1.235 +      I I (K false) (K []) (K false);
   1.236    in
   1.237      []
   1.238      |> Graph.fold (fn (name, (def, _)) =>