src/Tools/Code/code_scala.ML
changeset 38923 79d7f2b4cf71
parent 38922 ec2a8efd8990
child 38924 fcd1d0457e27
     1.1 --- a/src/Tools/Code/code_scala.ML	Tue Aug 31 13:15:35 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 13:29:38 2010 +0200
     1.3 @@ -24,14 +24,14 @@
     1.4  
     1.5  (** Scala serializer **)
     1.6  
     1.7 -fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
     1.8 +fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved
     1.9      args_num is_singleton_constr (deresolve, deresolve_full) =
    1.10    let
    1.11      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    1.12      fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    1.13      fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
    1.14            (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
    1.15 -    and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
    1.16 +    and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.17           of NONE => print_tyco_expr tyvars fxy (tyco, tys)
    1.18            | SOME (i, print) => print (print_typ tyvars) fxy tys)
    1.19        | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    1.20 @@ -67,7 +67,7 @@
    1.21            end 
    1.22        | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    1.23            (case Code_Thingol.unfold_const_app t0
    1.24 -           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    1.25 +           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.26                  then print_case tyvars some_thm vars fxy cases
    1.27                  else print_app tyvars is_pat some_thm vars fxy c_ts
    1.28              | NONE => print_case tyvars some_thm vars fxy cases)
    1.29 @@ -76,8 +76,8 @@
    1.30        let
    1.31          val k = length ts;
    1.32          val arg_typs' = if is_pat orelse
    1.33 -          (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
    1.34 -        val (l, print') = case syntax_const c
    1.35 +          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
    1.36 +        val (l, print') = case const_syntax c
    1.37           of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
    1.38                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.39                  (applify "[" "]" (print_typ tyvars NOBR)
    1.40 @@ -156,7 +156,7 @@
    1.41                fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
    1.42              val tyvars = reserved
    1.43                |> intro_base_names
    1.44 -                   (is_none o syntax_tyco) deresolve tycos
    1.45 +                   (is_none o tyco_syntax) deresolve tycos
    1.46                |> intro_tyvars vs;
    1.47              val simple = case eqs
    1.48               of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
    1.49 @@ -165,7 +165,7 @@
    1.50                (map (snd o fst) eqs) [];
    1.51              val vars1 = reserved
    1.52                |> intro_base_names
    1.53 -                   (is_none o syntax_const) deresolve consts
    1.54 +                   (is_none o const_syntax) deresolve consts
    1.55              val params = if simple
    1.56                then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
    1.57                else aux_params vars1 (map (fst o fst) eqs);
    1.58 @@ -414,7 +414,7 @@
    1.59    in (deresolver, sca_program) end;
    1.60  
    1.61  fun serialize_scala labelled_name raw_reserved includes module_alias
    1.62 -    _ syntax_tyco syntax_const
    1.63 +    _ tyco_syntax const_syntax
    1.64      program (stmt_names, presentation_stmt_names) =
    1.65    let
    1.66  
    1.67 @@ -440,7 +440,7 @@
    1.68      fun is_singleton_constr c = case Graph.get_node program c
    1.69       of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
    1.70        | _ => false;
    1.71 -    val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
    1.72 +    val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
    1.73        (make_vars reserved) args_num is_singleton_constr;
    1.74  
    1.75      (* print nodes *)
    1.76 @@ -524,7 +524,7 @@
    1.77          make_command = fn scala_home => fn _ =>
    1.78            "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
    1.79              ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
    1.80 -  #> Code_Target.add_syntax_tyco target "fun"
    1.81 +  #> Code_Target.add_tyco_syntax target "fun"
    1.82       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.83          brackify_infix (1, R) fxy (
    1.84            print_typ BR ty1 (*product type vs. tupled arguments!*),