src/Tools/Code/code_ml.ML
changeset 55684 ee49b4f7edc8
parent 55683 5732a55b9232
child 55776 7dd1971b39c1
     1.1 --- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  datatype ml_stmt =
     1.5      ML_Exc of string * (typscheme * int)
     1.6    | ML_Val of ml_binding
     1.7 -  | ML_Funs of ml_binding list * Code_Symbol.T list
     1.8 +  | ML_Funs of (Code_Namespace.export * ml_binding) list * Code_Symbol.T list
     1.9    | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
    1.10    | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
    1.11  
    1.12 @@ -260,7 +260,7 @@
    1.13              [sig_p]
    1.14              (semicolon [p])
    1.15            end
    1.16 -      | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
    1.17 +      | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) =
    1.18            let
    1.19              val print_def' = print_def (member (op =) pseudo_funs) false;
    1.20              fun print_pseudo_fun sym = concat [
    1.21 @@ -271,10 +271,11 @@
    1.22                  str "();"
    1.23                ];
    1.24              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
    1.25 -              (print_def' "fun" binding :: map (print_def' "and") bindings);
    1.26 +              (print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings);
    1.27              val pseudo_ps = map print_pseudo_fun pseudo_funs;
    1.28            in pair
    1.29 -            sig_ps
    1.30 +            (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE)
    1.31 +              ((export :: map fst exports_bindings) ~~ sig_ps))
    1.32              (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
    1.33            end
    1.34       | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
    1.35 @@ -605,7 +606,7 @@
    1.36              [sig_p]
    1.37              (doublesemicolon [p])
    1.38            end
    1.39 -      | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
    1.40 +      | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) =
    1.41            let
    1.42              val print_def' = print_def (member (op =) pseudo_funs) false;
    1.43              fun print_pseudo_fun sym = concat [
    1.44 @@ -616,10 +617,11 @@
    1.45                  str "();;"
    1.46                ];
    1.47              val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
    1.48 -              (print_def' "let rec" binding :: map (print_def' "and") bindings);
    1.49 +              (print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings);
    1.50              val pseudo_ps = map print_pseudo_fun pseudo_funs;
    1.51            in pair
    1.52 -            sig_ps
    1.53 +            (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE)
    1.54 +              ((export :: map fst exports_bindings) ~~ sig_ps))
    1.55              (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
    1.56            end
    1.57       | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
    1.58 @@ -667,7 +669,9 @@
    1.59                  )
    1.60                ];
    1.61            in pair
    1.62 -            (type_decl_p :: map print_classparam_decl classparams)
    1.63 +           (if Code_Namespace.is_public export
    1.64 +              then type_decl_p :: map print_classparam_decl classparams
    1.65 +              else [concat [str "type", print_dicttyp (class, ITyVar v)]])
    1.66              (Pretty.chunks (
    1.67                doublesemicolon [type_decl_p]
    1.68                :: map print_classparam_proj classparams
    1.69 @@ -733,7 +737,7 @@
    1.70        | namify_stmt (Code_Thingol.Classrel _) = namify_const false
    1.71        | namify_stmt (Code_Thingol.Classparam _) = namify_const false
    1.72        | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
    1.73 -    fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
    1.74 +    fun ml_binding_of_stmt (sym as Constant const, (export, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _))) =
    1.75            let
    1.76              val eqs = filter (snd o snd) raw_eqs;
    1.77              val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
    1.78 @@ -742,49 +746,58 @@
    1.79                    else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
    1.80                  | _ => (eqs, NONE)
    1.81                else (eqs, NONE)
    1.82 -          in (ML_Function (const, (tysm, eqs')), some_sym) end
    1.83 -      | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
    1.84 -          (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
    1.85 +          in ((export, ML_Function (const, (tysm, eqs'))), some_sym) end
    1.86 +      | ml_binding_of_stmt (sym as Class_Instance inst, (export, Code_Thingol.Classinst (stmt as { vs, ... }))) =
    1.87 +          ((export, ML_Instance (inst, stmt)),
    1.88 +            if forall (null o snd) vs then SOME (sym, false) else NONE)
    1.89        | ml_binding_of_stmt (sym, _) =
    1.90            error ("Binding block containing illegal statement: " ^ 
    1.91              Code_Symbol.quote ctxt sym)
    1.92 -    fun modify_fun (sym, stmt) =
    1.93 +    fun modify_fun (sym, (export, stmt)) =
    1.94        let
    1.95 -        val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
    1.96 +        val ((export', binding), some_value_sym) = ml_binding_of_stmt (sym, (export, stmt));
    1.97          val ml_stmt = case binding
    1.98           of ML_Function (const, ((vs, ty), [])) =>
    1.99                ML_Exc (const, ((vs, ty),
   1.100                  (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   1.101            | _ => case some_value_sym
   1.102 -             of NONE => ML_Funs ([binding], [])
   1.103 -              | SOME (sym, true) => ML_Funs ([binding], [sym])
   1.104 +             of NONE => ML_Funs ([(export', binding)], [])
   1.105 +              | SOME (sym, true) => ML_Funs ([(export, binding)], [sym])
   1.106                | SOME (sym, false) => ML_Val binding
   1.107 -      in SOME ml_stmt end;
   1.108 +      in SOME (export, ml_stmt) end;
   1.109      fun modify_funs stmts = single (SOME
   1.110 -      (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   1.111 -    fun modify_datatypes stmts = single (SOME
   1.112 -      (ML_Datas (map_filter
   1.113 -        (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   1.114 -    fun modify_class stmts = single (SOME
   1.115 -      (ML_Class (the_single (map_filter
   1.116 -        (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   1.117 -    fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
   1.118 +      (Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   1.119 +    fun modify_datatypes stmts =
   1.120 +      map_filter
   1.121 +        (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
   1.122 +      |> split_list
   1.123 +      |> apfst Code_Namespace.join_exports
   1.124 +      |> apsnd ML_Datas
   1.125 +      |> SOME
   1.126 +      |> single;
   1.127 +    fun modify_class stmts =
   1.128 +      the_single (map_filter
   1.129 +        (fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)
   1.130 +      |> apsnd ML_Class
   1.131 +      |> SOME
   1.132 +      |> single;
   1.133 +    fun modify_stmts ([stmt as (_, (_, stmt' as Code_Thingol.Fun _))]) =
   1.134            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   1.135 -      | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
   1.136 -          modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
   1.137 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
   1.138 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Fun _)) :: _)) =
   1.139 +          modify_funs (filter_out (Code_Thingol.is_case o snd o snd) stmts)
   1.140 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatypecons _)) :: _)) =
   1.141            modify_datatypes stmts
   1.142 -      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
   1.143 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatype _)) :: _)) =
   1.144            modify_datatypes stmts
   1.145 -      | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
   1.146 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Class _)) :: _)) =
   1.147            modify_class stmts
   1.148 -      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
   1.149 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Classrel _)) :: _)) =
   1.150            modify_class stmts
   1.151 -      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
   1.152 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Classparam _)) :: _)) =
   1.153            modify_class stmts
   1.154 -      | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   1.155 +      | modify_stmts ([stmt as (_, (_, Code_Thingol.Classinst _))]) =
   1.156            [modify_fun stmt]
   1.157 -      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
   1.158 +      | modify_stmts ((stmts as (_, (_, Code_Thingol.Classinst _)) :: _)) =
   1.159            modify_funs stmts
   1.160        | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   1.161            (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
   1.162 @@ -792,7 +805,9 @@
   1.163      Code_Namespace.hierarchical_program ctxt {
   1.164        module_name = module_name, reserved = reserved, identifiers = identifiers,
   1.165        empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   1.166 -      cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
   1.167 +      cyclic_modules = false, class_transitive = false,
   1.168 +      class_relation_public = true, empty_data = (),
   1.169 +      memorize_data = K I, modify_stmts = modify_stmts }
   1.170    end;
   1.171  
   1.172  fun serialize_ml print_ml_module print_ml_stmt ctxt