# HG changeset patch # User haftmann # Date 1466693196 -7200 # Node ID 705229ed856e5438174d73adbabf7ef20324a417 # Parent 6c889fe495a22942e6400cc80f9c0c3ce2c5829b compiling implicit instances into companion objects for classes avoids ambiguities diff -r 6c889fe495a2 -r 705229ed856e NEWS --- a/NEWS Wed Jun 22 19:01:26 2016 +0200 +++ b/NEWS Thu Jun 23 16:46:36 2016 +0200 @@ -129,6 +129,10 @@ different phases of code generation. See src/HOL/ex/Code_Timing.thy for examples. +* Code generator: implicits in Scala (stemming from type class instances) +are generated into companion object of corresponding type class, to resolve +some situations where ambiguities may occur. + *** HOL *** diff -r 6c889fe495a2 -r 705229ed856e src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Wed Jun 22 19:01:26 2016 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Jun 23 16:46:36 2016 +0200 @@ -13,8 +13,6 @@ structure Code_Scala : CODE_SCALA = struct -val target = "Scala"; - open Basic_Code_Symbol; open Basic_Code_Thingol; open Code_Printer; @@ -29,6 +27,15 @@ (** Scala serializer **) +val target = "Scala"; + +datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list + | Datatype of vname list * ((string * vname list) * itype list) list + | Class of (vname * ((class * class) list * (string * itype) list)) + * (string * { vs: (vname * sort) list, + inst_params: ((string * (const * int)) * (thm * bool)) list, + superinst_params: ((string * (const * int)) * (thm * bool)) list }) list; + fun print_scala_stmt tyco_syntax const_syntax reserved args_num is_constr (deresolve, deresolve_full) = let @@ -172,14 +179,14 @@ |> single |> enclose "(" ")" end; - fun print_context tyvars vs sym = applify "[" "]" + fun print_context tyvars vs s = applify "[" "]" (fn (v, sort) => (Pretty.block o map str) (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) - NOBR ((str o deresolve) sym) vs; + NOBR (str s) vs; fun print_defhead export tyvars vars const vs params tys ty = concat [str "def", constraint (applify "(" ")" (fn (param, ty) => constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) - NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty), + NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty), str "="]; fun print_def export const (vs, ty) [] = let @@ -233,9 +240,38 @@ (map print_clause eqs) end; val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant; - fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), raw_eqs), _))) = + fun print_inst class (tyco, { vs, inst_params, superinst_params }) = + let + val tyvars = intro_tyvars vs reserved; + val classtyp = (class, tyco `%% map (ITyVar o fst) vs); + fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) = + let + val aux_dom = Name.invent_names (snd reserved) "a" dom; + val auxs = map fst aux_dom; + val vars = intro_vars auxs reserved; + val (aux_dom1, aux_dom2) = chop dom_length aux_dom; + fun abstract_using [] = [] + | abstract_using aux_dom = [enum "," "(" ")" + (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) + (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; + val aux_abstr1 = abstract_using aux_dom1; + val aux_abstr2 = abstract_using aux_dom2; + in + concat ([str "val", print_method classparam, str "="] + @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR + (const, map (IVar o SOME) auxs)) + end; + in + Pretty.block_enclose (concat [str "implicit def", + constraint (print_context tyvars vs + ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class))) + (print_dicttyp tyvars classtyp), + str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") + (map print_classparam_instance (inst_params @ superinst_params)) + end; + fun print_stmt (Constant const, (export, Fun ((vs, ty), raw_eqs))) = print_def export const (vs, ty) (filter (snd o snd) raw_eqs) - | print_stmt (Type_Constructor tyco, (export, Code_Thingol.Datatype (vs, cos))) = + | print_stmt (Type_Constructor tyco, (export, Datatype (vs, cos))) = let val tyvars = intro_tyvars (map (rpair []) vs) reserved; fun print_co ((co, vs_args), tys) = @@ -252,7 +288,7 @@ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs :: map print_co cos) end - | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) = + | print_stmt (Type_Class class, (export, Class ((v, (classrels, classparams)), insts))) = let val tyvars = intro_tyvars [(v, [class])] reserved; fun add_typarg s = Pretty.block @@ -286,38 +322,24 @@ @ the_list (print_super_classes classrels) @ [str "{"]), str "}") (map print_classparam_val classparams)) :: map print_classparam_def classparams + @| Pretty.block_enclose + ((concat o map str) ["object", deresolve_class class, "{"], str "}") + (map (print_inst class) insts) ) - end - | print_stmt (sym, (export, Code_Thingol.Classinst - { class, tyco, vs, inst_params, superinst_params, ... })) = - let - val tyvars = intro_tyvars vs reserved; - val classtyp = (class, tyco `%% map (ITyVar o fst) vs); - fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) = - let - val aux_dom = Name.invent_names (snd reserved) "a" dom; - val auxs = map fst aux_dom; - val vars = intro_vars auxs reserved; - val (aux_dom1, aux_dom2) = chop dom_length aux_dom; - fun abstract_using [] = [] - | abstract_using aux_dom = [enum "," "(" ")" - (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) - (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; - val aux_abstr1 = abstract_using aux_dom1; - val aux_abstr2 = abstract_using aux_dom2; - in - concat ([str "val", print_method classparam, str "="] - @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR - (const, map (IVar o SOME) auxs)) - end; - in - Pretty.block_enclose (concat [str "implicit def", - constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp), - str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") - (map print_classparam_instance (inst_params @ superinst_params)) end; in print_stmt end; +fun pickup_instances_for_class program = + let + val tab = + Symtab.empty + |> Code_Symbol.Graph.fold + (fn (_, (Code_Thingol.Classinst { class, tyco, vs, inst_params, superinst_params, ... }, _)) => + Symtab.map_default (class, []) + (cons (tyco, { vs = vs, inst_params = inst_params, superinst_params = superinst_params })) + | _ => I) program; + in Symtab.lookup_list tab end; + fun scala_program_of_program ctxt module_name reserved identifiers exports program = let val variant = if Config.get ctxt case_insensitive @@ -348,26 +370,24 @@ | namify_stmt (Code_Thingol.Classrel _) = namify_object | namify_stmt (Code_Thingol.Classparam _) = namify_object | namify_stmt (Code_Thingol.Classinst _) = namify_common; - fun memorize_implicits sym = - let - fun is_classinst stmt = case stmt - of Code_Thingol.Classinst _ => true - | _ => false; - val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program) - (Code_Symbol.Graph.immediate_succs program sym); - in union (op =) implicits end; + val pickup_instances = pickup_instances_for_class program; fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE + | modify_stmt (_, (export, Code_Thingol.Fun (x, NONE))) = SOME (export, Fun x) + | modify_stmt (_, (export, Code_Thingol.Datatype x)) = SOME (export, Datatype x) | modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE + | modify_stmt (Type_Class class, (export, Code_Thingol.Class x)) = + SOME (export, Class (x, pickup_instances class)) | modify_stmt (_, (_, Code_Thingol.Classrel _)) = NONE | modify_stmt (_, (_, Code_Thingol.Classparam _)) = NONE - | modify_stmt (_, export_stmt) = SOME export_stmt; + | modify_stmt (_, (_, Code_Thingol.Classinst _)) = NONE in Code_Namespace.hierarchical_program ctxt { module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt, cyclic_modules = true, - class_transitive = true, class_relation_public = false, empty_data = [], - memorize_data = memorize_implicits, modify_stmts = map modify_stmt } exports program + class_transitive = true, class_relation_public = false, empty_data = (), + memorize_data = K I, modify_stmts = map modify_stmt } + exports program end; fun serialize_scala ctxt { module_name, reserved_syms, identifiers, @@ -398,16 +418,9 @@ (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []); (* print modules *) - fun print_implicit prefix_fragments implicit = - let - val s = deresolver prefix_fragments implicit; - in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end; - fun print_module prefix_fragments base implicits ps = Pretty.chunks2 - ([str ("object " ^ base ^ " {")] - @ (case map_filter (print_implicit prefix_fragments) implicits - of [] => [] | implicit_ps => (single o Pretty.block) - (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps)) - @ ps @ [str ("} /* object " ^ base ^ " */")]); + fun print_module _ base _ ps = Pretty.chunks2 + (str ("object " ^ base ^ " {") + :: ps @| str ("} /* object " ^ base ^ " */")); (* serialization *) val p = Pretty.chunks2 (map snd includes