src/Tools/Code/code_ml.ML
changeset 39028 0dd6c5a0beef
parent 38966 68853347ba37
child 39031 b27d6643591c
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 10:29:48 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 10:29:48 2010 +0200
     1.3 @@ -707,6 +707,87 @@
     1.4  
     1.5  (** SML/OCaml generic part **)
     1.6  
     1.7 +fun ml_program_of_program labelled_name reserved module_alias program =
     1.8 +  let
     1.9 +    fun namify_const upper base (nsp_const, nsp_type) =
    1.10 +      let
    1.11 +        val (base', nsp_const') = yield_singleton Name.variants
    1.12 +          (if upper then first_upper base else base) nsp_const
    1.13 +      in (base', (nsp_const', nsp_type)) end;
    1.14 +    fun namify_type base (nsp_const, nsp_type) =
    1.15 +      let
    1.16 +        val (base', nsp_type') = yield_singleton Name.variants base nsp_type
    1.17 +      in (base', (nsp_const, nsp_type')) end;
    1.18 +    fun namify_stmt (Code_Thingol.Fun _) = namify_const false
    1.19 +      | namify_stmt (Code_Thingol.Datatype _) = namify_type
    1.20 +      | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
    1.21 +      | namify_stmt (Code_Thingol.Class _) = namify_type
    1.22 +      | namify_stmt (Code_Thingol.Classrel _) = namify_const false
    1.23 +      | namify_stmt (Code_Thingol.Classparam _) = namify_const false
    1.24 +      | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
    1.25 +    fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
    1.26 +          let
    1.27 +            val eqs = filter (snd o snd) raw_eqs;
    1.28 +            val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
    1.29 +               of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
    1.30 +                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
    1.31 +                  else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
    1.32 +                | _ => (eqs, NONE)
    1.33 +              else (eqs, NONE)
    1.34 +          in (ML_Function (name, (tysm, eqs')), some_value_name) end
    1.35 +      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
    1.36 +          (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
    1.37 +      | ml_binding_of_stmt (name, _) =
    1.38 +          error ("Binding block containing illegal statement: " ^ labelled_name name)
    1.39 +    fun modify_fun (name, stmt) =
    1.40 +      let
    1.41 +        val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
    1.42 +        val ml_stmt = case binding
    1.43 +         of ML_Function (name, ((vs, ty), [])) =>
    1.44 +              ML_Exc (name, ((vs, ty),
    1.45 +                (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
    1.46 +          | _ => case some_value_name
    1.47 +             of NONE => ML_Funs ([binding], [])
    1.48 +              | SOME (name, true) => ML_Funs ([binding], [name])
    1.49 +              | SOME (name, false) => ML_Val binding
    1.50 +      in SOME ml_stmt end;
    1.51 +    fun modify_funs stmts =
    1.52 +      (SOME (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))
    1.53 +        :: replicate (length stmts - 1) NONE)
    1.54 +    fun modify_datatypes stmts =
    1.55 +      (SOME (ML_Datas (map_filter
    1.56 +        (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))
    1.57 +        :: replicate (length stmts - 1) NONE)
    1.58 +    fun modify_class stmts =
    1.59 +      (SOME (ML_Class (the_single (map_filter
    1.60 +        (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
    1.61 +        :: replicate (length stmts - 1) NONE)
    1.62 +    fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
    1.63 +          [modify_fun stmt]
    1.64 +      | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
    1.65 +          modify_funs stmts
    1.66 +      | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
    1.67 +          modify_datatypes stmts
    1.68 +      | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
    1.69 +          modify_datatypes stmts
    1.70 +      | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
    1.71 +          modify_class stmts
    1.72 +      | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
    1.73 +          modify_class stmts
    1.74 +      | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
    1.75 +          modify_class stmts
    1.76 +      | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
    1.77 +          [modify_fun stmt]
    1.78 +      | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
    1.79 +          modify_funs stmts
    1.80 +      | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
    1.81 +          (Library.commas o map (labelled_name o fst)) stmts);
    1.82 +  in
    1.83 +    Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
    1.84 +      empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
    1.85 +      cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
    1.86 +  end;
    1.87 +
    1.88  local
    1.89  
    1.90  datatype ml_node =
    1.91 @@ -906,27 +987,30 @@
    1.92    let
    1.93      val is_cons = Code_Thingol.is_cons program;
    1.94      val is_presentation = not (null presentation_names);
    1.95 -    val (deresolver, nodes) = ml_node_of_program labelled_name
    1.96 -      reserved_syms module_alias program;
    1.97 -    val reserved = make_vars reserved_syms;
    1.98 -    fun print_node prefix (Dummy _) =
    1.99 +    val { deresolver, hierarchical_program = ml_program } =
   1.100 +      ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   1.101 +    fun print_node _ (_, Code_Namespace.Dummy) =
   1.102            NONE
   1.103 -      | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   1.104 -          (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
   1.105 +      | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) =
   1.106 +          if is_presentation andalso
   1.107 +            (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
   1.108            then NONE
   1.109 -          else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
   1.110 -      | print_node prefix (Module (module_name, (_, nodes))) =
   1.111 +          else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
   1.112 +            is_cons (deresolver prefix_fragments) stmt)
   1.113 +      | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
   1.114            let
   1.115 -            val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   1.116 +            val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
   1.117              val p = if is_presentation then Pretty.chunks2 body
   1.118 -              else print_module module_name (if with_signatures then SOME decls else NONE) body;
   1.119 +              else print_module name_fragment
   1.120 +                (if with_signatures then SOME decls else NONE) body;
   1.121            in SOME ([], p) end
   1.122 -    and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
   1.123 +    and print_nodes prefix_fragments nodes = (map_filter
   1.124 +        (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
   1.125          o rev o flat o Graph.strong_conn) nodes
   1.126        |> split_list
   1.127        |> (fn (decls, body) => (flat decls, body))
   1.128      val names' = map (try (deresolver [])) names;
   1.129 -    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   1.130 +    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
   1.131      fun write width NONE = writeln_pretty width
   1.132        | write width (SOME p) = File.write p o string_of_pretty width;
   1.133    in