src/Tools/Code/code_scala.ML
changeset 55147 bce3dbc11f95
parent 55145 2bb3cd36bcf7
child 55150 0940309ed8f1
     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 @@ -27,15 +27,18 @@
     1.4  fun print_scala_stmt tyco_syntax const_syntax reserved
     1.5      args_num is_constr (deresolve, deresolve_full) =
     1.6    let
     1.7 +    val deresolve_const = deresolve o Code_Symbol.Constant;
     1.8 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
     1.9 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    1.10      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    1.11      fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    1.12 -    fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
    1.13 -          (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
    1.14 +    fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
    1.15 +          (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
    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 +         of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys)
    1.19            | SOME (_, print) => print (print_typ tyvars) fxy tys)
    1.20        | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    1.21 -    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
    1.22 +    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
    1.23      fun print_tupled_typ tyvars ([], ty) =
    1.24            print_typ tyvars NOBR ty
    1.25        | print_tupled_typ tyvars ([ty1], ty2) =
    1.26 @@ -67,20 +70,24 @@
    1.27            end
    1.28        | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
    1.29            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.30 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    1.31 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    1.32 +                if is_none (const_syntax const)
    1.33                  then print_case tyvars some_thm vars fxy case_expr
    1.34                  else print_app tyvars is_pat some_thm vars fxy app
    1.35              | NONE => print_case tyvars some_thm vars fxy case_expr)
    1.36      and print_app tyvars is_pat some_thm vars fxy
    1.37 -        (app as ({ name = c, typargs, dom, ... }, ts)) =
    1.38 +        (app as ({ sym, typargs, dom, ... }, ts)) =
    1.39        let
    1.40          val k = length ts;
    1.41          val typargs' = if is_pat then [] else typargs;
    1.42 -        val (l, print') = case const_syntax c
    1.43 -         of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")"
    1.44 +        val syntax = case sym of
    1.45 +            Code_Symbol.Constant const => const_syntax const
    1.46 +          | _ => NONE;
    1.47 +        val (l, print') = case syntax of
    1.48 +            NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
    1.49                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.50                  (applify "[" "]" (print_typ tyvars NOBR)
    1.51 -                  NOBR ((str o deresolve) c) typargs') ts)
    1.52 +                  NOBR ((str o deresolve) sym) typargs') ts)
    1.53            | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    1.54                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.55                  (applify "[" "]" (print_typ tyvars NOBR)
    1.56 @@ -137,32 +144,32 @@
    1.57              |> single
    1.58              |> enclose "(" ")"
    1.59            end;
    1.60 -    fun print_context tyvars vs name = applify "[" "]"
    1.61 +    fun print_context tyvars vs sym = applify "[" "]"
    1.62        (fn (v, sort) => (Pretty.block o map str)
    1.63 -        (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
    1.64 -          NOBR ((str o deresolve) name) vs;
    1.65 -    fun print_defhead tyvars vars name vs params tys ty =
    1.66 +        (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
    1.67 +          NOBR ((str o deresolve) sym) vs;
    1.68 +    fun print_defhead tyvars vars const vs params tys ty =
    1.69        Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
    1.70          constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
    1.71 -          NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
    1.72 +          NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
    1.73              str " ="];
    1.74 -    fun print_def name (vs, ty) [] =
    1.75 +    fun print_def const (vs, ty) [] =
    1.76            let
    1.77              val (tys, ty') = Code_Thingol.unfold_fun ty;
    1.78              val params = Name.invent (snd reserved) "a" (length tys);
    1.79              val tyvars = intro_tyvars vs reserved;
    1.80              val vars = intro_vars params reserved;
    1.81            in
    1.82 -            concat [print_defhead tyvars vars name vs params tys ty',
    1.83 -              str ("sys.error(\"" ^ name ^ "\")")]
    1.84 +            concat [print_defhead tyvars vars const vs params tys ty',
    1.85 +              str ("sys.error(\"" ^ const ^ "\")")]
    1.86            end
    1.87 -      | print_def name (vs, ty) eqs =
    1.88 +      | print_def const (vs, ty) eqs =
    1.89            let
    1.90              val tycos = fold (fn ((ts, t), _) =>
    1.91                fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
    1.92              val tyvars = reserved
    1.93                |> intro_base_names
    1.94 -                   (is_none o tyco_syntax) deresolve tycos
    1.95 +                   (is_none o tyco_syntax) deresolve_tyco tycos
    1.96                |> intro_tyvars vs;
    1.97              val simple = case eqs
    1.98               of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
    1.99 @@ -188,7 +195,7 @@
   1.100                    tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
   1.101                    str "=>", print_rhs vars' eq]
   1.102                end;
   1.103 -            val head = print_defhead tyvars vars2 name vs params tys' ty';
   1.104 +            val head = print_defhead tyvars vars2 const vs params tys' ty';
   1.105            in if simple then
   1.106              concat [head, print_rhs vars2 (hd eqs)]
   1.107            else
   1.108 @@ -197,34 +204,34 @@
   1.109                  str "match", str "{"], str "}")
   1.110                (map print_clause eqs)
   1.111            end;
   1.112 -    val print_method = str o Library.enclose "`" "`" o deresolve_full;
   1.113 -    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
   1.114 -          print_def name (vs, ty) (filter (snd o snd) raw_eqs)
   1.115 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
   1.116 +    val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant;
   1.117 +    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
   1.118 +          print_def const (vs, ty) (filter (snd o snd) raw_eqs)
   1.119 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
   1.120            let
   1.121              val tyvars = intro_tyvars (map (rpair []) vs) reserved;
   1.122              fun print_co ((co, vs_args), tys) =
   1.123                concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
   1.124 -                ((concat o map str) ["final", "case", "class", deresolve co]) vs_args)
   1.125 +                ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
   1.126                  @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
   1.127                    (Name.invent_names (snd reserved) "a" tys))),
   1.128                  str "extends",
   1.129                  applify "[" "]" (str o lookup_tyvar tyvars) NOBR
   1.130 -                  ((str o deresolve) name) vs
   1.131 +                  ((str o deresolve_tyco) tyco) vs
   1.132                ];
   1.133            in
   1.134              Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
   1.135 -              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
   1.136 +              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
   1.137                  :: map print_co cos)
   1.138            end
   1.139 -      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   1.140 +      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
   1.141            let
   1.142 -            val tyvars = intro_tyvars [(v, [name])] reserved;
   1.143 +            val tyvars = intro_tyvars [(v, [class])] reserved;
   1.144              fun add_typarg s = Pretty.block
   1.145                [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
   1.146              fun print_super_classes [] = NONE
   1.147 -              | print_super_classes classes = SOME (concat (str "extends"
   1.148 -                  :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
   1.149 +              | print_super_classes classrels = SOME (concat (str "extends"
   1.150 +                  :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
   1.151              fun print_classparam_val (classparam, ty) =
   1.152                concat [str "val", constraint (print_method classparam)
   1.153                  ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
   1.154 @@ -238,22 +245,22 @@
   1.155                in
   1.156                  concat [str "def", constraint (Pretty.block [applify "(" ")"
   1.157                    (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   1.158 -                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
   1.159 +                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
   1.160                    (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
   1.161 -                  add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
   1.162 +                  add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
   1.163                    applify "(" ")" (str o lookup_var vars) NOBR
   1.164                    (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
   1.165                end;
   1.166            in
   1.167              Pretty.chunks (
   1.168                (Pretty.block_enclose
   1.169 -                (concat ([str "trait", (add_typarg o deresolve) name]
   1.170 -                  @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
   1.171 +                (concat ([str "trait", (add_typarg o deresolve_class) class]
   1.172 +                  @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
   1.173                  (map print_classparam_val classparams))
   1.174                :: map print_classparam_def classparams
   1.175              )
   1.176            end
   1.177 -      | print_stmt (name, Code_Thingol.Classinst
   1.178 +      | print_stmt (sym, Code_Thingol.Classinst
   1.179            { class, tyco, vs, inst_params, superinst_params, ... }) =
   1.180            let
   1.181              val tyvars = intro_tyvars vs reserved;
   1.182 @@ -277,13 +284,13 @@
   1.183                end;
   1.184            in
   1.185              Pretty.block_enclose (concat [str "implicit def",
   1.186 -              constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
   1.187 +              constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
   1.188                str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   1.189                  (map print_classparam_instance (inst_params @ superinst_params))
   1.190            end;
   1.191    in print_stmt end;
   1.192  
   1.193 -fun scala_program_of_program ctxt symbol_of module_name reserved identifiers program =
   1.194 +fun scala_program_of_program ctxt module_name reserved identifiers program =
   1.195    let
   1.196      fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
   1.197        let
   1.198 @@ -312,49 +319,49 @@
   1.199        | namify_stmt (Code_Thingol.Classrel _) = namify_object
   1.200        | namify_stmt (Code_Thingol.Classparam _) = namify_object
   1.201        | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
   1.202 -    fun memorize_implicits name =
   1.203 +    fun memorize_implicits sym =
   1.204        let
   1.205          fun is_classinst stmt = case stmt
   1.206           of Code_Thingol.Classinst _ => true
   1.207            | _ => false;
   1.208 -        val implicits = filter (is_classinst o Graph.get_node program)
   1.209 -          (Graph.immediate_succs program name);
   1.210 +        val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program)
   1.211 +          (Code_Symbol.Graph.immediate_succs program sym);
   1.212        in union (op =) implicits end;
   1.213 -    fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
   1.214 +    fun modify_stmt (_, Code_Thingol.Fun (_, SOME _)) = NONE
   1.215        | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
   1.216        | modify_stmt (_, Code_Thingol.Classrel _) = NONE
   1.217        | modify_stmt (_, Code_Thingol.Classparam _) = NONE
   1.218        | modify_stmt (_, stmt) = SOME stmt;
   1.219    in
   1.220 -    Code_Namespace.hierarchical_program ctxt symbol_of
   1.221 +    Code_Namespace.hierarchical_program ctxt
   1.222        { module_name = module_name, reserved = reserved, identifiers = identifiers,
   1.223          empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
   1.224          namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
   1.225          memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
   1.226    end;
   1.227  
   1.228 -fun serialize_scala ctxt { symbol_of, module_name, reserved_syms, identifiers,
   1.229 +fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
   1.230      includes, class_syntax, tyco_syntax, const_syntax } program =
   1.231    let
   1.232  
   1.233      (* build program *)
   1.234      val { deresolver, hierarchical_program = scala_program } =
   1.235 -      scala_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
   1.236 +      scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
   1.237  
   1.238      (* print statements *)
   1.239 -    fun lookup_constr tyco constr = case Graph.get_node program tyco
   1.240 -     of Code_Thingol.Datatype (_, (_, constrs)) =>
   1.241 +    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
   1.242 +     of Code_Thingol.Datatype (_, constrs) =>
   1.243            the (AList.lookup (op = o apsnd fst) constrs constr);
   1.244 -    fun classparams_of_class class = case Graph.get_node program class
   1.245 -     of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
   1.246 -    fun args_num c = case Graph.get_node program c
   1.247 -     of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
   1.248 +    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class)
   1.249 +     of Code_Thingol.Class (_, (_, classparams)) => classparams;
   1.250 +    fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym
   1.251 +     of Code_Thingol.Fun (((_, ty), []), _) =>
   1.252            (length o fst o Code_Thingol.unfold_fun) ty
   1.253 -      | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   1.254 -      | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
   1.255 -      | Code_Thingol.Classparam (_, class) =>
   1.256 +      | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
   1.257 +      | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const)
   1.258 +      | Code_Thingol.Classparam class =>
   1.259            (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
   1.260 -            (classparams_of_class class)) c;
   1.261 +            (classparams_of_class class)) const;
   1.262      fun print_stmt prefix_fragments = print_scala_stmt
   1.263        tyco_syntax const_syntax (make_vars reserved_syms) args_num
   1.264        (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
   1.265 @@ -378,7 +385,7 @@
   1.266          lift_markup = I } scala_program);
   1.267      fun write width NONE = writeln o format [] width
   1.268        | write width (SOME p) = File.write p o format [] width;
   1.269 -    fun prepare names width p = ([("", format names width p)], try (deresolver []));
   1.270 +    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
   1.271    in
   1.272      Code_Target.serialization write prepare p
   1.273    end;