src/Tools/Code/code_scala.ML
changeset 55150 0940309ed8f1
parent 55147 bce3dbc11f95
child 55153 eedd549de3ef
     1.1 --- a/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4  
     1.5  val target = "Scala";
     1.6  
     1.7 +open Basic_Code_Symbol;
     1.8  open Basic_Code_Thingol;
     1.9  open Code_Printer;
    1.10  
    1.11 @@ -27,18 +28,18 @@
    1.12  fun print_scala_stmt tyco_syntax const_syntax reserved
    1.13      args_num is_constr (deresolve, deresolve_full) =
    1.14    let
    1.15 -    val deresolve_const = deresolve o Code_Symbol.Constant;
    1.16 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    1.17 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    1.18 +    val deresolve_const = deresolve o Constant;
    1.19 +    val deresolve_tyco = deresolve o Type_Constructor;
    1.20 +    val deresolve_class = deresolve o Type_Class;
    1.21      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    1.22      fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    1.23      fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
    1.24            (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
    1.25      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.26 -         of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys)
    1.27 +         of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
    1.28            | SOME (_, print) => print (print_typ tyvars) fxy tys)
    1.29        | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    1.30 -    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
    1.31 +    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
    1.32      fun print_tupled_typ tyvars ([], ty) =
    1.33            print_typ tyvars NOBR ty
    1.34        | print_tupled_typ tyvars ([ty1], ty2) =
    1.35 @@ -70,7 +71,7 @@
    1.36            end
    1.37        | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
    1.38            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.39 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    1.40 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
    1.41                  if is_none (const_syntax const)
    1.42                  then print_case tyvars some_thm vars fxy case_expr
    1.43                  else print_app tyvars is_pat some_thm vars fxy app
    1.44 @@ -81,7 +82,7 @@
    1.45          val k = length ts;
    1.46          val typargs' = if is_pat then [] else typargs;
    1.47          val syntax = case sym of
    1.48 -            Code_Symbol.Constant const => const_syntax const
    1.49 +            Constant const => const_syntax const
    1.50            | _ => NONE;
    1.51          val (l, print') = case syntax of
    1.52              NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
    1.53 @@ -151,7 +152,7 @@
    1.54      fun print_defhead tyvars vars const vs params tys ty =
    1.55        Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
    1.56          constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
    1.57 -          NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
    1.58 +          NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
    1.59              str " ="];
    1.60      fun print_def const (vs, ty) [] =
    1.61            let
    1.62 @@ -204,10 +205,10 @@
    1.63                  str "match", str "{"], str "}")
    1.64                (map print_clause eqs)
    1.65            end;
    1.66 -    val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant;
    1.67 -    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    1.68 +    val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
    1.69 +    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    1.70            print_def const (vs, ty) (filter (snd o snd) raw_eqs)
    1.71 -      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
    1.72 +      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
    1.73            let
    1.74              val tyvars = intro_tyvars (map (rpair []) vs) reserved;
    1.75              fun print_co ((co, vs_args), tys) =
    1.76 @@ -224,7 +225,7 @@
    1.77                NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
    1.78                  :: map print_co cos)
    1.79            end
    1.80 -      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    1.81 +      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    1.82            let
    1.83              val tyvars = intro_tyvars [(v, [class])] reserved;
    1.84              fun add_typarg s = Pretty.block
    1.85 @@ -349,12 +350,12 @@
    1.86        scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
    1.87  
    1.88      (* print statements *)
    1.89 -    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
    1.90 +    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
    1.91       of Code_Thingol.Datatype (_, constrs) =>
    1.92            the (AList.lookup (op = o apsnd fst) constrs constr);
    1.93 -    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class)
    1.94 +    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class)
    1.95       of Code_Thingol.Class (_, (_, classparams)) => classparams;
    1.96 -    fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym
    1.97 +    fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
    1.98       of Code_Thingol.Fun (((_, ty), []), _) =>
    1.99            (length o fst o Code_Thingol.unfold_fun) ty
   1.100        | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
   1.101 @@ -422,7 +423,7 @@
   1.102          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
   1.103          make_command = fn _ =>
   1.104            "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
   1.105 -  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   1.106 +  #> Code_Target.set_printings (Type_Constructor ("fun",
   1.107      [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.108        brackify_infix (1, R) fxy (
   1.109          print_typ BR ty1 (*product type vs. tupled arguments!*),