# HG changeset patch # User haftmann # Date 1283416393 -7200 # Node ID b27d6643591c111e91a6b150459ddee53a446e1d # Parent 2bb34f36db808fb0ef5ad1390a8225727bcca579 dropped dead code; tuned diff -r 2bb34f36db80 -r b27d6643591c src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Sep 02 10:29:50 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Sep 02 10:33:13 2010 +0200 @@ -751,17 +751,14 @@ | SOME (name, true) => ML_Funs ([binding], [name]) | SOME (name, false) => ML_Val binding in SOME ml_stmt end; - fun modify_funs stmts = - (SOME (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)) - :: replicate (length stmts - 1) NONE) - fun modify_datatypes stmts = - (SOME (ML_Datas (map_filter - (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)) - :: replicate (length stmts - 1) NONE) - fun modify_class stmts = - (SOME (ML_Class (the_single (map_filter - (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))) - :: replicate (length stmts - 1) NONE) + fun modify_funs stmts = single (SOME + (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))) + fun modify_datatypes stmts = single (SOME + (ML_Datas (map_filter + (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))) + fun modify_class stmts = single (SOME + (ML_Class (the_single (map_filter + (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))) fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) = [modify_fun stmt] | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = @@ -788,199 +785,6 @@ cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program end; -local - -datatype ml_node = - Dummy of string - | Stmt of string * ml_stmt - | Module of string * ((Name.context * Name.context) * ml_node Graph.T); - -in - -fun ml_node_of_program labelled_name reserved module_alias program = - let - val reserved = Name.make_context reserved; - val empty_module = ((reserved, reserved), Graph.empty); - fun map_node [] f = f - | map_node (m::ms) f = - Graph.default_node (m, Module (m, empty_module)) - #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) => - Module (module_name, (nsp, map_node ms f nodes))); - fun map_nsp_yield [] f (nsp, nodes) = - let - val (x, nsp') = f nsp - in (x, (nsp', nodes)) end - | map_nsp_yield (m::ms) f (nsp, nodes) = - let - val (x, nodes') = - nodes - |> Graph.default_node (m, Module (m, empty_module)) - |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => - let - val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes - in (x, Module (d_module_name, nsp_nodes')) end) - in (x, (nsp, nodes')) end; - fun map_nsp_fun_yield f (nsp_fun, nsp_typ) = - let - val (x, nsp_fun') = f nsp_fun - in (x, (nsp_fun', nsp_typ)) end; - fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = - let - val (x, nsp_typ') = f nsp_typ - in (x, (nsp_fun, nsp_typ')) end; - val mk_name_module = mk_name_module reserved NONE module_alias program; - fun mk_name_stmt upper name nsp = - let - val (_, base) = dest_name name; - val base' = if upper then first_upper base else base; - val ([base''], nsp') = Name.variants [base'] nsp; - in (base'', nsp') end; - fun deps_of names = - [] - |> fold (fold (insert (op =)) o Graph.imm_succs program) names - |> subtract (op =) names - |> filter_out (Code_Thingol.is_case o Graph.get_node program); - fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) = - let - val eqs = filter (snd o snd) raw_eqs; - val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs - of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty - then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) - else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) - | _ => (eqs, NONE) - else (eqs, NONE) - in (ML_Function (name, (tysm, eqs')), is_value) end - | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = - (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE) - | ml_binding_of_stmt (name, _) = - error ("Binding block containing illegal statement: " ^ labelled_name name) - fun add_fun (name, stmt) = - let - val (binding, some_value_name) = ml_binding_of_stmt (name, stmt); - val ml_stmt = case binding - of ML_Function (name, ((vs, ty), [])) => - ML_Exc (name, ((vs, ty), - (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) - | _ => case some_value_name - of NONE => ML_Funs ([binding], []) - | SOME (name, true) => ML_Funs ([binding], [name]) - | SOME (name, false) => ML_Val binding - in - map_nsp_fun_yield (mk_name_stmt false name) - #>> (fn name' => ([name'], ml_stmt)) - end; - fun add_funs stmts = - let - val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst); - in - fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts - #>> rpair ml_stmt - end; - fun add_datatypes stmts = - fold_map - (fn (name, Code_Thingol.Datatype (_, stmt)) => - map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) - | (name, Code_Thingol.Datatypecons _) => - map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE - | (name, _) => - error ("Datatype block containing illegal statement: " ^ labelled_name name) - ) stmts - #>> (split_list #> apsnd (map_filter I - #> (fn [] => error ("Datatype block without data statement: " - ^ (Library.commas o map (labelled_name o fst)) stmts) - | stmts => ML_Datas stmts))); - fun add_class stmts = - fold_map - (fn (name, Code_Thingol.Class (_, stmt)) => - map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) - | (name, Code_Thingol.Classrel _) => - map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE - | (name, Code_Thingol.Classparam _) => - map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE - | (name, _) => - error ("Class block containing illegal statement: " ^ labelled_name name) - ) stmts - #>> (split_list #> apsnd (map_filter I - #> (fn [] => error ("Class block without class statement: " - ^ (Library.commas o map (labelled_name o fst)) stmts) - | [stmt] => ML_Class stmt))); - fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) = - add_fun stmt - | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = - add_funs stmts - | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = - add_datatypes stmts - | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) = - add_datatypes stmts - | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) = - add_class stmts - | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) = - add_class stmts - | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) = - add_class stmts - | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) = - add_fun stmt - | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) = - add_funs stmts - | add_stmts stmts = error ("Illegal mutual dependencies: " ^ - (Library.commas o map (labelled_name o fst)) stmts); - fun add_stmts' stmts nsp_nodes = - let - val names as (name :: names') = map fst stmts; - val deps = deps_of names; - val (module_names, _) = (split_list o map dest_name) names; - val module_name = (the_single o distinct (op =) o map mk_name_module) module_names - handle Empty => - error ("Different namespace prefixes for mutual dependencies:\n" - ^ Library.commas (map labelled_name names) - ^ "\n" - ^ Library.commas module_names); - val module_name_path = Long_Name.explode module_name; - fun add_dep name name' = - let - val module_name' = (mk_name_module o fst o dest_name) name'; - in if module_name = module_name' then - map_node module_name_path (Graph.add_edge (name, name')) - else let - val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =) - (module_name_path, Long_Name.explode module_name'); - in - map_node common - (fn node => Graph.add_edge_acyclic (diff1, diff2) node - handle Graph.CYCLES _ => error ("Dependency " - ^ quote name ^ " -> " ^ quote name' - ^ " would result in module dependency cycle")) - end end; - in - nsp_nodes - |> map_nsp_yield module_name_path (add_stmts stmts) - |-> (fn (base' :: bases', stmt') => - apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt'))) - #> fold2 (fn name' => fn base' => - Graph.new_node (name', (Dummy base'))) names' bases'))) - |> apsnd (fold (fn name => fold (add_dep name) deps) names) - |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names) - end; - val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program)) - |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false); - val (_, nodes) = fold add_stmts' stmts empty_module; - fun deresolver prefix name = - let - val module_name = (fst o dest_name) name; - val module_name' = (Long_Name.explode o mk_name_module) module_name; - val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); - val stmt_name = - nodes - |> fold (fn name => fn node => case Graph.get_node node name - of Module (_, (_, node)) => node) module_name' - |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name - | Dummy stmt_name => stmt_name); - in - Long_Name.implode (remainder @ [stmt_name]) - end handle Graph.UNDEF _ => - error ("Unknown statement name: " ^ labelled_name name); - in (deresolver, nodes) end; - fun serialize_ml target print_module print_stmt with_signatures { labelled_name, reserved_syms, includes, module_alias, class_syntax, tyco_syntax, const_syntax, program, names, presentation_names } = @@ -1017,8 +821,6 @@ Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p end; -end; (*local*) - val serializer_sml : Code_Target.serializer = Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true >> (fn with_signatures => serialize_ml target_SML