first serious draft of a scala code generator
authorhaftmann
Thu Jun 17 15:59:48 2010 +0200 (2010-06-17)
changeset 3745045073611170a
parent 37449 034ebe92f090
child 37451 3058c918e7a3
first serious draft of a scala code generator
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_scala.ML	Thu Jun 17 15:59:47 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jun 17 15:59:48 2010 +0200
     1.3 @@ -61,18 +61,18 @@
     1.4                  then print_case tyvars some_thm vars fxy cases
     1.5                  else print_app tyvars is_pat some_thm vars fxy c_ts
     1.6              | NONE => print_case tyvars some_thm vars fxy cases)
     1.7 -    and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
     1.8 +    and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((arg_typs, _), function_typs)), ts)) =
     1.9        let
    1.10          val k = length ts;
    1.11          val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
    1.12 -        val tys' = if is_pat orelse
    1.13 -          (is_none (syntax_const c) andalso is_singleton c) then [] else tys;
    1.14 +        val arg_typs' = if is_pat orelse
    1.15 +          (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
    1.16          val (no_syntax, print') = case syntax_const c
    1.17           of NONE => (true, fn ts => applify "(" ")" fxy
    1.18 -              (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
    1.19 +              (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) arg_typs'))
    1.20                  (map (print_term tyvars is_pat some_thm vars NOBR) ts))
    1.21            | SOME (_, print) => (false, fn ts =>
    1.22 -              print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l tys_args));
    1.23 +              print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l function_typs));
    1.24        in if k = l then print' ts
    1.25        else if k < l then
    1.26          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    1.27 @@ -122,10 +122,11 @@
    1.28          val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
    1.29            implicit_names implicit_typ_ps;
    1.30        in ((implicit_names, implicit_ps), vars') end;
    1.31 -    fun print_defhead tyvars vars p vs params tys implicits ty =
    1.32 +    fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
    1.33        Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
    1.34          (applify "(" ")" NOBR
    1.35 -          (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
    1.36 +          (applify "[" "]" NOBR p (map (fn (v, sort) =>
    1.37 +              (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
    1.38              (map2 (fn param => fn ty => print_typed tyvars
    1.39                  ((str o lookup_var vars) param) ty)
    1.40                params tys)) implicits) ty, str " ="]
    1.41 @@ -156,7 +157,7 @@
    1.42                  val vars1 = reserved
    1.43                    |> intro_base_names
    1.44                         (is_none o syntax_const) deresolve consts
    1.45 -                val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1;
    1.46 +                val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1; (*FIXME drop*)
    1.47                  val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
    1.48                    else aux_params vars2 (map (fst o fst) eqs);
    1.49                  val vars3 = intro_vars params vars2;
    1.50 @@ -174,7 +175,7 @@
    1.51                      concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
    1.52                        str "=>", print_rhs vars' eq]
    1.53                    end;
    1.54 -                val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
    1.55 +                val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 [] ty2;
    1.56                in if simple then
    1.57                  concat [head, print_rhs vars3 (hd eqs)]
    1.58                else
    1.59 @@ -186,23 +187,25 @@
    1.60        | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
    1.61            let
    1.62              val tyvars = intro_vars (map fst vs) reserved;
    1.63 -            fun print_co (co, []) =
    1.64 +            fun print_co ((co, _), []) =
    1.65                    concat [str "final", str "case", str "object", (str o deresolve_base) co,
    1.66                      str "extends", applify "[" "]" NOBR ((str o deresolve_base) name)
    1.67                        (replicate (length vs) (str "Nothing"))]
    1.68 -              | print_co (co, tys) =
    1.69 +              | print_co ((co, vs_args), tys) =
    1.70                    let
    1.71                      val fields = Name.names (snd reserved) "a" tys;
    1.72                      val vars = intro_vars (map fst fields) reserved;
    1.73 -                    fun add_typargs p = applify "[" "]" NOBR p
    1.74 -                      (map (str o lookup_tyvar tyvars o fst) vs);
    1.75 +                    fun add_typargs1 p = applify "[" "]" NOBR p
    1.76 +                      (map (str o lookup_tyvar tyvars o fst) vs); (*FIXME*)
    1.77 +                    fun add_typargs2 p = applify "[" "]" NOBR p
    1.78 +                      (map (str o lookup_tyvar tyvars) vs_args); (*FIXME*)
    1.79                    in
    1.80                      concat [
    1.81                        applify "(" ")" NOBR
    1.82 -                        (add_typargs ((concat o map str) ["final", "case", "class", deresolve_base co]))
    1.83 +                        (add_typargs2 ((concat o map str) ["final", "case", "class", deresolve_base co]))
    1.84                          (map (uncurry (print_typed tyvars) o apfst str) fields),
    1.85                        str "extends",
    1.86 -                      add_typargs ((str o deresolve_base) name)
    1.87 +                      add_typargs1 ((str o deresolve_base) name)
    1.88                      ]
    1.89                    end
    1.90            in
    1.91 @@ -230,13 +233,24 @@
    1.92              fun print_classparam_val (classparam, ty) =
    1.93                concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
    1.94                  (print_tupled_typ o Code_Thingol.unfold_fun) ty]
    1.95 +            fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
    1.96 +              let
    1.97 +                val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
    1.98 +                  [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
    1.99 +                val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
   1.100 +                  lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
   1.101 +                val vars' = intro_vars implicit_names vars;
   1.102 +                val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
   1.103 +                  implicit_names implicit_typ_ps;
   1.104 +              in ((implicit_names, implicit_ps), vars') end;
   1.105              fun print_classparam_def (classparam, ty) =
   1.106                let
   1.107                  val (tys, ty) = Code_Thingol.unfold_fun ty;
   1.108                  val params = Name.invents (snd reserved) "a" (length tys);
   1.109                  val vars = intro_vars params reserved;
   1.110                  val (([implicit], [p_implicit]), vars') = implicit_arguments tyvars vs vars;
   1.111 -                val head = print_defhead tyvars vars' ((str o deresolve) classparam) vs params tys [p_implicit] ty;
   1.112 +                val head = print_defhead tyvars vars' ((str o deresolve) classparam)
   1.113 +                  ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
   1.114                in
   1.115                  concat [head, applify "(" ")" NOBR
   1.116                    (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
   1.117 @@ -252,9 +266,39 @@
   1.118              )
   1.119            end
   1.120        | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
   1.121 -            (super_instances, classparam_instances))) =
   1.122 +            (super_instances, (classparam_instances, further_classparam_instances)))) =
   1.123            let
   1.124              val tyvars = intro_vars (map fst vs) reserved;
   1.125 +            val classtyp = (class, (tyco, map fst vs));
   1.126 +            fun print_classtyp' (class, (tyco, vs)) = (*FIXME already exists?*)
   1.127 +              applify "[" "]" NOBR(*? FIXME*) ((str o deresolve) class)
   1.128 +                [print_typ tyvars NOBR (tyco `%% map ITyVar vs)]; (*FIXME a mess...*)
   1.129 +            fun print_typed' tyvars p classtyp = (*FIXME unify with existing print_typed*)
   1.130 +              Pretty.block [p, str ":", Pretty.brk 1, print_classtyp' classtyp];
   1.131 +            fun print_defhead' tyvars vars p vs params tys classtyp = (*FIXME unify with existing def_head*)
   1.132 +              Pretty.block [str "def ", print_typed' tyvars
   1.133 +                (applify "(" ")" NOBR
   1.134 +                  (applify "[" "]" NOBR p (map (fn (v, sort) =>
   1.135 +                      (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
   1.136 +                    (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty)
   1.137 +                      params tys)) classtyp, str " ="];
   1.138 +            fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   1.139 +              let
   1.140 +                val auxs = Name.invents (snd reserved) "a" (length tys);
   1.141 +                val vars = intro_vars auxs reserved;
   1.142 +                val args = if null auxs then [] else
   1.143 +                  [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
   1.144 +                    auxs tys), str "=>"]];
   1.145 +              in 
   1.146 +                concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
   1.147 +                  str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
   1.148 +              end;
   1.149 +            val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
   1.150 +            val body = [str "new", print_classtyp' classtyp,
   1.151 +              Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
   1.152 +          in concat (str "implicit" :: head :: body) end;
   1.153 +          (*let
   1.154 +            val tyvars = intro_vars (map fst vs) reserved;
   1.155              val insttyp = tyco `%% map (ITyVar o fst) vs;
   1.156              val p_inst_typ = print_typ tyvars NOBR insttyp;
   1.157              fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
   1.158 @@ -291,7 +335,7 @@
   1.159                      Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
   1.160                        implicit_names)]
   1.161              ]
   1.162 -          end;
   1.163 +          end;*)
   1.164    in print_stmt end;
   1.165  
   1.166  fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   1.167 @@ -356,14 +400,14 @@
   1.168        | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   1.169        | Code_Thingol.Datatypecons (_, tyco) =>
   1.170            let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   1.171 -          in (length o the o AList.lookup (op =) constrs) c end
   1.172 +          in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   1.173        | Code_Thingol.Classparam (_, class) =>
   1.174            let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
   1.175            in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
   1.176      fun is_singleton c = case Graph.get_node program c
   1.177       of Code_Thingol.Datatypecons (_, tyco) =>
   1.178            let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   1.179 -          in (null o the o AList.lookup (op =) constrs) c end
   1.180 +          in (null o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   1.181        | _ => false;
   1.182      val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   1.183        reserved args_num is_singleton deresolver;