src/Tools/Code/code_ml.ML
changeset 39031 b27d6643591c
parent 39028 0dd6c5a0beef
child 39034 ebeb48fd653b
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 10:29:50 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 10:33:13 2010 +0200
     1.3 @@ -751,17 +751,14 @@
     1.4                | SOME (name, true) => ML_Funs ([binding], [name])
     1.5                | SOME (name, false) => ML_Val binding
     1.6        in SOME ml_stmt end;
     1.7 -    fun modify_funs stmts =
     1.8 -      (SOME (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))
     1.9 -        :: replicate (length stmts - 1) NONE)
    1.10 -    fun modify_datatypes stmts =
    1.11 -      (SOME (ML_Datas (map_filter
    1.12 -        (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))
    1.13 -        :: replicate (length stmts - 1) NONE)
    1.14 -    fun modify_class stmts =
    1.15 -      (SOME (ML_Class (the_single (map_filter
    1.16 -        (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
    1.17 -        :: replicate (length stmts - 1) NONE)
    1.18 +    fun modify_funs stmts = single (SOME
    1.19 +      (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
    1.20 +    fun modify_datatypes stmts = single (SOME
    1.21 +      (ML_Datas (map_filter
    1.22 +        (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
    1.23 +    fun modify_class stmts = single (SOME
    1.24 +      (ML_Class (the_single (map_filter
    1.25 +        (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
    1.26      fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
    1.27            [modify_fun stmt]
    1.28        | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
    1.29 @@ -788,199 +785,6 @@
    1.30        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
    1.31    end;
    1.32  
    1.33 -local
    1.34 -
    1.35 -datatype ml_node =
    1.36 -    Dummy of string
    1.37 -  | Stmt of string * ml_stmt
    1.38 -  | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
    1.39 -
    1.40 -in
    1.41 -
    1.42 -fun ml_node_of_program labelled_name reserved module_alias program =
    1.43 -  let
    1.44 -    val reserved = Name.make_context reserved;
    1.45 -    val empty_module = ((reserved, reserved), Graph.empty);
    1.46 -    fun map_node [] f = f
    1.47 -      | map_node (m::ms) f =
    1.48 -          Graph.default_node (m, Module (m, empty_module))
    1.49 -          #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
    1.50 -               Module (module_name, (nsp, map_node ms f nodes)));
    1.51 -    fun map_nsp_yield [] f (nsp, nodes) =
    1.52 -          let
    1.53 -            val (x, nsp') = f nsp
    1.54 -          in (x, (nsp', nodes)) end
    1.55 -      | map_nsp_yield (m::ms) f (nsp, nodes) =
    1.56 -          let
    1.57 -            val (x, nodes') =
    1.58 -              nodes
    1.59 -              |> Graph.default_node (m, Module (m, empty_module))
    1.60 -              |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
    1.61 -                  let
    1.62 -                    val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
    1.63 -                  in (x, Module (d_module_name, nsp_nodes')) end)
    1.64 -          in (x, (nsp, nodes')) end;
    1.65 -    fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
    1.66 -      let
    1.67 -        val (x, nsp_fun') = f nsp_fun
    1.68 -      in (x, (nsp_fun', nsp_typ)) end;
    1.69 -    fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
    1.70 -      let
    1.71 -        val (x, nsp_typ') = f nsp_typ
    1.72 -      in (x, (nsp_fun, nsp_typ')) end;
    1.73 -    val mk_name_module = mk_name_module reserved NONE module_alias program;
    1.74 -    fun mk_name_stmt upper name nsp =
    1.75 -      let
    1.76 -        val (_, base) = dest_name name;
    1.77 -        val base' = if upper then first_upper base else base;
    1.78 -        val ([base''], nsp') = Name.variants [base'] nsp;
    1.79 -      in (base'', nsp') end;
    1.80 -    fun deps_of names =
    1.81 -      []
    1.82 -      |> fold (fold (insert (op =)) o Graph.imm_succs program) names
    1.83 -      |> subtract (op =) names
    1.84 -      |> filter_out (Code_Thingol.is_case o Graph.get_node program);
    1.85 -    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
    1.86 -          let
    1.87 -            val eqs = filter (snd o snd) raw_eqs;
    1.88 -            val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
    1.89 -               of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
    1.90 -                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
    1.91 -                  else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
    1.92 -                | _ => (eqs, NONE)
    1.93 -              else (eqs, NONE)
    1.94 -          in (ML_Function (name, (tysm, eqs')), is_value) end
    1.95 -      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
    1.96 -          (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
    1.97 -      | ml_binding_of_stmt (name, _) =
    1.98 -          error ("Binding block containing illegal statement: " ^ labelled_name name)
    1.99 -    fun add_fun (name, stmt) =
   1.100 -      let
   1.101 -        val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   1.102 -        val ml_stmt = case binding
   1.103 -         of ML_Function (name, ((vs, ty), [])) =>
   1.104 -              ML_Exc (name, ((vs, ty),
   1.105 -                (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   1.106 -          | _ => case some_value_name
   1.107 -             of NONE => ML_Funs ([binding], [])
   1.108 -              | SOME (name, true) => ML_Funs ([binding], [name])
   1.109 -              | SOME (name, false) => ML_Val binding
   1.110 -      in
   1.111 -        map_nsp_fun_yield (mk_name_stmt false name)
   1.112 -        #>> (fn name' => ([name'], ml_stmt))
   1.113 -      end;
   1.114 -    fun add_funs stmts =
   1.115 -      let
   1.116 -        val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
   1.117 -      in
   1.118 -        fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
   1.119 -        #>> rpair ml_stmt
   1.120 -      end;
   1.121 -    fun add_datatypes stmts =
   1.122 -      fold_map
   1.123 -        (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   1.124 -              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   1.125 -          | (name, Code_Thingol.Datatypecons _) =>
   1.126 -              map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   1.127 -          | (name, _) =>
   1.128 -              error ("Datatype block containing illegal statement: " ^ labelled_name name)
   1.129 -        ) stmts
   1.130 -      #>> (split_list #> apsnd (map_filter I
   1.131 -        #> (fn [] => error ("Datatype block without data statement: "
   1.132 -                  ^ (Library.commas o map (labelled_name o fst)) stmts)
   1.133 -             | stmts => ML_Datas stmts)));
   1.134 -    fun add_class stmts =
   1.135 -      fold_map
   1.136 -        (fn (name, Code_Thingol.Class (_, stmt)) =>
   1.137 -              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   1.138 -          | (name, Code_Thingol.Classrel _) =>
   1.139 -              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   1.140 -          | (name, Code_Thingol.Classparam _) =>
   1.141 -              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   1.142 -          | (name, _) =>
   1.143 -              error ("Class block containing illegal statement: " ^ labelled_name name)
   1.144 -        ) stmts
   1.145 -      #>> (split_list #> apsnd (map_filter I
   1.146 -        #> (fn [] => error ("Class block without class statement: "
   1.147 -                  ^ (Library.commas o map (labelled_name o fst)) stmts)
   1.148 -             | [stmt] => ML_Class stmt)));
   1.149 -    fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   1.150 -          add_fun stmt
   1.151 -      | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   1.152 -          add_funs stmts
   1.153 -      | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   1.154 -          add_datatypes stmts
   1.155 -      | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   1.156 -          add_datatypes stmts
   1.157 -      | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   1.158 -          add_class stmts
   1.159 -      | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   1.160 -          add_class stmts
   1.161 -      | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   1.162 -          add_class stmts
   1.163 -      | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   1.164 -          add_fun stmt
   1.165 -      | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   1.166 -          add_funs stmts
   1.167 -      | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   1.168 -          (Library.commas o map (labelled_name o fst)) stmts);
   1.169 -    fun add_stmts' stmts nsp_nodes =
   1.170 -      let
   1.171 -        val names as (name :: names') = map fst stmts;
   1.172 -        val deps = deps_of names;
   1.173 -        val (module_names, _) = (split_list o map dest_name) names;
   1.174 -        val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   1.175 -          handle Empty =>
   1.176 -            error ("Different namespace prefixes for mutual dependencies:\n"
   1.177 -              ^ Library.commas (map labelled_name names)
   1.178 -              ^ "\n"
   1.179 -              ^ Library.commas module_names);
   1.180 -        val module_name_path = Long_Name.explode module_name;
   1.181 -        fun add_dep name name' =
   1.182 -          let
   1.183 -            val module_name' = (mk_name_module o fst o dest_name) name';
   1.184 -          in if module_name = module_name' then
   1.185 -            map_node module_name_path (Graph.add_edge (name, name'))
   1.186 -          else let
   1.187 -            val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   1.188 -              (module_name_path, Long_Name.explode module_name');
   1.189 -          in
   1.190 -            map_node common
   1.191 -              (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   1.192 -                handle Graph.CYCLES _ => error ("Dependency "
   1.193 -                  ^ quote name ^ " -> " ^ quote name'
   1.194 -                  ^ " would result in module dependency cycle"))
   1.195 -          end end;
   1.196 -      in
   1.197 -        nsp_nodes
   1.198 -        |> map_nsp_yield module_name_path (add_stmts stmts)
   1.199 -        |-> (fn (base' :: bases', stmt') =>
   1.200 -           apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   1.201 -              #> fold2 (fn name' => fn base' =>
   1.202 -                   Graph.new_node (name', (Dummy base'))) names' bases')))
   1.203 -        |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   1.204 -        |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   1.205 -      end;
   1.206 -    val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program))
   1.207 -      |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false);
   1.208 -    val (_, nodes) = fold add_stmts' stmts empty_module;
   1.209 -    fun deresolver prefix name = 
   1.210 -      let
   1.211 -        val module_name = (fst o dest_name) name;
   1.212 -        val module_name' = (Long_Name.explode o mk_name_module) module_name;
   1.213 -        val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   1.214 -        val stmt_name =
   1.215 -          nodes
   1.216 -          |> fold (fn name => fn node => case Graph.get_node node name
   1.217 -              of Module (_, (_, node)) => node) module_name'
   1.218 -          |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   1.219 -               | Dummy stmt_name => stmt_name);
   1.220 -      in
   1.221 -        Long_Name.implode (remainder @ [stmt_name])
   1.222 -      end handle Graph.UNDEF _ =>
   1.223 -        error ("Unknown statement name: " ^ labelled_name name);
   1.224 -  in (deresolver, nodes) end;
   1.225 -
   1.226  fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
   1.227    reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
   1.228    const_syntax, program, names, presentation_names } =
   1.229 @@ -1017,8 +821,6 @@
   1.230      Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
   1.231    end;
   1.232  
   1.233 -end; (*local*)
   1.234 -
   1.235  val serializer_sml : Code_Target.serializer =
   1.236    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   1.237    >> (fn with_signatures => serialize_ml target_SML