src/Tools/code/code_ml.ML
changeset 28663 bd8438543bf2
parent 28350 715163ec93c0
child 28673 d746a8c12c43
     1.1 --- a/src/Tools/code/code_ml.ML	Wed Oct 22 14:15:44 2008 +0200
     1.2 +++ b/src/Tools/code/code_ml.ML	Wed Oct 22 14:15:45 2008 +0200
     1.3 @@ -42,15 +42,15 @@
     1.4  
     1.5  (** SML serailizer **)
     1.6  
     1.7 -fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
     1.8 +fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
     1.9    let
    1.10      val pr_label_classrel = translate_string (fn "." => "__" | c => c)
    1.11        o NameSpace.qualifier;
    1.12      val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
    1.13      fun pr_dicts fxy ds =
    1.14        let
    1.15 -        fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
    1.16 -          | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
    1.17 +        fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
    1.18 +          | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
    1.19          fun pr_proj [] p =
    1.20                p
    1.21            | pr_proj [p'] p =
    1.22 @@ -86,7 +86,7 @@
    1.23      fun pr_term thm pat vars fxy (IConst c) =
    1.24            pr_app thm pat vars fxy (c, [])
    1.25        | pr_term thm pat vars fxy (IVar v) =
    1.26 -          str (lookup_var vars v)
    1.27 +          str (Code_Name.lookup_var vars v)
    1.28        | pr_term thm pat vars fxy (t as t1 `$ t2) =
    1.29            (case Code_Thingol.unfold_const_app t
    1.30             of SOME c_ts => pr_app thm pat vars fxy c_ts
    1.31 @@ -116,7 +116,7 @@
    1.32        else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
    1.33          (str o deresolve) c
    1.34            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
    1.35 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
    1.36 +    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
    1.37      and pr_bind' ((NONE, NONE), _) = str "_"
    1.38        | pr_bind' ((SOME v, NONE), _) = str v
    1.39        | pr_bind' ((NONE, SOME p), _) = p
    1.40 @@ -199,8 +199,8 @@
    1.41                              then NONE else (SOME o NameSpace.base o deresolve) c)
    1.42                              ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
    1.43                          val vars = reserved_names
    1.44 -                          |> intro_vars consts
    1.45 -                          |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
    1.46 +                          |> Code_Name.intro_vars consts
    1.47 +                          |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
    1.48                                 (insert (op =)) ts []);
    1.49                        in
    1.50                          concat (
    1.51 @@ -250,7 +250,7 @@
    1.52            in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
    1.53       | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
    1.54            let
    1.55 -            val w = first_upper v ^ "_";
    1.56 +            val w = Code_Name.first_upper v ^ "_";
    1.57              fun pr_superclass_field (class, classrel) =
    1.58                (concat o map str) [
    1.59                  pr_label_classrel classrel, ":", "'" ^ v, deresolve class
    1.60 @@ -342,12 +342,12 @@
    1.61  
    1.62  (** OCaml serializer **)
    1.63  
    1.64 -fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
    1.65 +fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    1.66    let
    1.67      fun pr_dicts fxy ds =
    1.68        let
    1.69 -        fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
    1.70 -          | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
    1.71 +        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
    1.72 +          | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
    1.73          fun pr_proj ps p =
    1.74            fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
    1.75          fun pr_dict fxy (DictConst (inst, dss)) =
    1.76 @@ -379,7 +379,7 @@
    1.77      fun pr_term thm pat vars fxy (IConst c) =
    1.78            pr_app thm pat vars fxy (c, [])
    1.79        | pr_term thm pat vars fxy (IVar v) =
    1.80 -          str (lookup_var vars v)
    1.81 +          str (Code_Name.lookup_var vars v)
    1.82        | pr_term thm pat vars fxy (t as t1 `$ t2) =
    1.83            (case Code_Thingol.unfold_const_app t
    1.84             of SOME c_ts => pr_app thm pat vars fxy c_ts
    1.85 @@ -407,7 +407,7 @@
    1.86          else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
    1.87        else (str o deresolve) c
    1.88          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
    1.89 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
    1.90 +    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
    1.91      and pr_bind' ((NONE, NONE), _) = str "_"
    1.92        | pr_bind' ((SOME v, NONE), _) = str v
    1.93        | pr_bind' ((NONE, SOME p), _) = p
    1.94 @@ -449,8 +449,8 @@
    1.95          val x = Name.variant (map_filter I fished1) "x";
    1.96          val fished2 = map_index (fillup_param x) fished1;
    1.97          val (fished3, _) = Name.variants fished2 Name.context;
    1.98 -        val vars' = intro_vars fished3 vars;
    1.99 -      in map (lookup_var vars') fished3 end;
   1.100 +        val vars' = Code_Name.intro_vars fished3 vars;
   1.101 +      in map (Code_Name.lookup_var vars') fished3 end;
   1.102      fun pr_stmt (MLFuns (funns as funn :: funns')) =
   1.103            let
   1.104              fun pr_eq ((ts, t), (thm, _)) =
   1.105 @@ -460,8 +460,8 @@
   1.106                      then NONE else (SOME o NameSpace.base o deresolve) c)
   1.107                      ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.108                  val vars = reserved_names
   1.109 -                  |> intro_vars consts
   1.110 -                  |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   1.111 +                  |> Code_Name.intro_vars consts
   1.112 +                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   1.113                        (insert (op =)) ts []);
   1.114                in concat [
   1.115                  (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   1.116 @@ -488,8 +488,8 @@
   1.117                          then NONE else (SOME o NameSpace.base o deresolve) c)
   1.118                          ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   1.119                      val vars = reserved_names
   1.120 -                      |> intro_vars consts
   1.121 -                      |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   1.122 +                      |> Code_Name.intro_vars consts
   1.123 +                      |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   1.124                            (insert (op =)) ts []);
   1.125                    in
   1.126                      concat (
   1.127 @@ -516,7 +516,7 @@
   1.128                          ((fold o Code_Thingol.fold_constnames)
   1.129                            (insert (op =)) (map (snd o fst) eqs) []);
   1.130                      val vars = reserved_names
   1.131 -                      |> intro_vars consts;
   1.132 +                      |> Code_Name.intro_vars consts;
   1.133                      val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
   1.134                    in
   1.135                      Pretty.block (
   1.136 @@ -574,7 +574,7 @@
   1.137            in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   1.138       | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   1.139            let
   1.140 -            val w = "_" ^ first_upper v;
   1.141 +            val w = "_" ^ Code_Name.first_upper v;
   1.142              fun pr_superclass_field (class, classrel) =
   1.143                (concat o map str) [
   1.144                  deresolve classrel, ":", "'" ^ v, deresolve class
   1.145 @@ -716,16 +716,16 @@
   1.146        let
   1.147          val (x, nsp_typ') = f nsp_typ
   1.148        in (x, (nsp_fun, nsp_typ')) end;
   1.149 -    val mk_name_module = mk_name_module reserved_names NONE module_alias program;
   1.150 +    val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
   1.151      fun mk_name_stmt upper name nsp =
   1.152        let
   1.153 -        val (_, base) = dest_name name;
   1.154 -        val base' = if upper then first_upper base else base;
   1.155 +        val (_, base) = Code_Name.dest_name name;
   1.156 +        val base' = if upper then Code_Name.first_upper base else base;
   1.157          val ([base''], nsp') = Name.variants [base'] nsp;
   1.158        in (base'', nsp') end;
   1.159      fun add_funs stmts =
   1.160        fold_map
   1.161 -        (fn (name, Code_Thingol.Fun stmt) =>
   1.162 +        (fn (name, Code_Thingol.Fun (_, stmt)) =>
   1.163                map_nsp_fun_yield (mk_name_stmt false name) #>>
   1.164                  rpair (name, stmt |> apsnd (filter (snd o snd)))
   1.165            | (name, _) =>
   1.166 @@ -734,7 +734,7 @@
   1.167        #>> (split_list #> apsnd MLFuns);
   1.168      fun add_datatypes stmts =
   1.169        fold_map
   1.170 -        (fn (name, Code_Thingol.Datatype stmt) =>
   1.171 +        (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   1.172                map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   1.173            | (name, Code_Thingol.Datatypecons _) =>
   1.174                map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   1.175 @@ -747,8 +747,8 @@
   1.176               | stmts => MLDatas stmts)));
   1.177      fun add_class stmts =
   1.178        fold_map
   1.179 -        (fn (name, Code_Thingol.Class info) =>
   1.180 -              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
   1.181 +        (fn (name, Code_Thingol.Class (_, stmt)) =>
   1.182 +              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   1.183            | (name, Code_Thingol.Classrel _) =>
   1.184                map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   1.185            | (name, Code_Thingol.Classparam _) =>
   1.186 @@ -786,7 +786,7 @@
   1.187            []
   1.188            |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   1.189            |> subtract (op =) names;
   1.190 -        val (module_names, _) = (split_list o map dest_name) names;
   1.191 +        val (module_names, _) = (split_list o map Code_Name.dest_name) names;
   1.192          val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   1.193            handle Empty =>
   1.194              error ("Different namespace prefixes for mutual dependencies:\n"
   1.195 @@ -796,7 +796,7 @@
   1.196          val module_name_path = NameSpace.explode module_name;
   1.197          fun add_dep name name' =
   1.198            let
   1.199 -            val module_name' = (mk_name_module o fst o dest_name) name';
   1.200 +            val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
   1.201            in if module_name = module_name' then
   1.202              map_node module_name_path (Graph.add_edge (name, name'))
   1.203            else let
   1.204 @@ -824,7 +824,7 @@
   1.205            (rev (Graph.strong_conn program)));
   1.206      fun deresolver prefix name = 
   1.207        let
   1.208 -        val module_name = (fst o dest_name) name;
   1.209 +        val module_name = (fst o Code_Name.dest_name) name;
   1.210          val module_name' = (NameSpace.explode o mk_name_module) module_name;
   1.211          val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   1.212          val stmt_name =
   1.213 @@ -840,19 +840,19 @@
   1.214    in (deresolver, nodes) end;
   1.215  
   1.216  fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
   1.217 -  _ syntax_tyco syntax_const program cs destination =
   1.218 +  _ syntax_tyco syntax_const naming program cs destination =
   1.219    let
   1.220      val is_cons = Code_Thingol.is_cons program;
   1.221      val stmt_names = Code_Target.stmt_names_of_destination destination;
   1.222      val module_name = if null stmt_names then raw_module_name else SOME "Code";
   1.223      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   1.224        reserved_names raw_module_alias program;
   1.225 -    val reserved_names = make_vars reserved_names;
   1.226 +    val reserved_names = Code_Name.make_vars reserved_names;
   1.227      fun pr_node prefix (Dummy _) =
   1.228            NONE
   1.229        | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
   1.230            (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
   1.231 -            (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
   1.232 +            (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
   1.233                (deresolver prefix) is_cons stmt)
   1.234            else NONE
   1.235        | pr_node prefix (Module (module_name, (_, nodes))) =
   1.236 @@ -861,8 +861,8 @@
   1.237                o rev o flat o Graph.strong_conn) nodes)
   1.238            |> (if null stmt_names then pr_module module_name else Pretty.chunks)
   1.239            |> SOME;
   1.240 -    val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
   1.241 -      cs;
   1.242 +    val cs' = (map o try)
   1.243 +      (deresolver (if is_some module_name then the_list module_name else [])) cs;
   1.244      val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
   1.245        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
   1.246    in
   1.247 @@ -877,8 +877,8 @@
   1.248  
   1.249  (** ML (system language) code for evaluation and instrumentalization **)
   1.250  
   1.251 -fun ml_code_of thy = Code_Target.serialize_custom thy
   1.252 -  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   1.253 +fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,
   1.254 +    (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   1.255    literals_sml));
   1.256  
   1.257  
   1.258 @@ -890,15 +890,16 @@
   1.259      val _ = if null (term_frees (term_of ct)) then () else error ("Term "
   1.260        ^ quote (Syntax.string_of_term_global thy (term_of ct))
   1.261        ^ " to be evaluated contains free variables");
   1.262 -    fun eval' program ((vs, ty), t) deps =
   1.263 +    fun eval' naming program ((vs, ty), t) deps =
   1.264        let
   1.265          val _ = if Code_Thingol.contains_dictvar t then
   1.266            error "Term to be evaluated constains free dictionaries" else ();
   1.267 +        val value_name = "Value.VALUE.value"
   1.268          val program' = program
   1.269 -          |> Graph.new_node (Code_Name.value_name,
   1.270 -              Code_Thingol.Fun (([], ty), [(([], t), (Drule.dummy_thm, true))]))
   1.271 -          |> fold (curry Graph.add_edge Code_Name.value_name) deps;
   1.272 -        val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
   1.273 +          |> Graph.new_node (value_name,
   1.274 +              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
   1.275 +          |> fold (curry Graph.add_edge value_name) deps;
   1.276 +        val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
   1.277          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
   1.278            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
   1.279        in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
   1.280 @@ -922,12 +923,13 @@
   1.281  
   1.282  fun delayed_code thy consts () =
   1.283    let
   1.284 -    val (consts', program) = Code_Thingol.consts_program thy consts;
   1.285 -    val (ml_code, consts'') = ml_code_of thy program consts';
   1.286 -    val _ = if length consts <> length consts'' then
   1.287 -      error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts)
   1.288 -        ^ "\nhas a user-defined serialization") else ();
   1.289 -  in (ml_code, consts ~~ consts'') end;
   1.290 +    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
   1.291 +    val (ml_code, consts'') = ml_code_of thy naming program consts';
   1.292 +    val const_tab = map2 (fn const => fn NONE =>
   1.293 +      error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
   1.294 +        ^ "\nhas a user-defined serialization")
   1.295 +      | SOME const' => (const, const')) consts consts''
   1.296 +  in (ml_code, const_tab) end;
   1.297  
   1.298  fun register_const const ctxt =
   1.299    let