src/Tools/code/code_target.ML
changeset 24591 6509626eb2c9
parent 24423 ae9cd0e92423
child 24621 97d403d9ab54
     1.1 --- a/src/Tools/code/code_target.ML	Sat Sep 15 19:27:48 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Sat Sep 15 19:27:50 2007 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    val assert_serializer: theory -> string -> string;
     1.5  
     1.6    val eval_verbose: bool ref;
     1.7 -  val eval_term: theory -> (string * 'a option ref) -> CodeThingol.code
     1.8 +  val eval_term: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
     1.9      ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.10    val code_width: int ref;
    1.11  
    1.12 @@ -298,7 +298,7 @@
    1.13    | MLClass of string * ((class * string) list * (vname * (string * itype) list))
    1.14    | MLClassinst of string * ((class * (string * (vname * sort) list))
    1.15          * ((class * (string * (string * dict list list))) list
    1.16 -      * (string * iterm) list));
    1.17 +      * (string * const) list));
    1.18  
    1.19  fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    1.20    let
    1.21 @@ -540,20 +540,12 @@
    1.22                  str "=",
    1.23                  pr_dicts NOBR [DictConst dss]
    1.24                ];
    1.25 -            fun pr_classop (classop, t) =
    1.26 -              let
    1.27 -                val consts = map_filter
    1.28 -                  (fn c => if (is_some o const_syntax) c
    1.29 -                    then NONE else (SOME o NameSpace.base o deresolv) c)
    1.30 -                    (CodeThingol.fold_constnames (insert (op =)) t []);
    1.31 -                val vars = CodeName.intro_vars consts init_syms;
    1.32 -              in
    1.33 -                concat [
    1.34 -                  (str o pr_label_classop) classop,
    1.35 -                  str "=",
    1.36 -                  pr_term false vars NOBR t
    1.37 -                ]
    1.38 -              end;
    1.39 +            fun pr_classop (classop, c_inst) =
    1.40 +              concat [
    1.41 +                (str o pr_label_classop) classop,
    1.42 +                str "=",
    1.43 +                pr_app false init_syms NOBR (c_inst, [])
    1.44 +              ];
    1.45            in
    1.46              semicolon ([
    1.47                str (if null arity then "val" else "fun"),
    1.48 @@ -831,20 +823,12 @@
    1.49                  str "=",
    1.50                  pr_dicts NOBR [DictConst dss]
    1.51                ];
    1.52 -            fun pr_classop_def (classop, t) =
    1.53 -              let
    1.54 -                val consts = map_filter
    1.55 -                  (fn c => if (is_some o const_syntax) c
    1.56 -                    then NONE else (SOME o NameSpace.base o deresolv) c)
    1.57 -                    (CodeThingol.fold_constnames (insert (op =)) t []);
    1.58 -                val vars = CodeName.intro_vars consts init_syms;
    1.59 -              in
    1.60 -                concat [
    1.61 -                  (str o deresolv) classop,
    1.62 -                  str "=",
    1.63 -                  pr_term false vars NOBR t
    1.64 -                ]
    1.65 -              end;
    1.66 +            fun pr_classop_def (classop, c_inst) =
    1.67 +              concat [
    1.68 +                (str o deresolv) classop,
    1.69 +                str "=",
    1.70 +                pr_app false init_syms NOBR (c_inst, [])
    1.71 +              ];
    1.72            in
    1.73              concat (
    1.74                str "let"
    1.75 @@ -920,7 +904,7 @@
    1.76      fun mk_funs defs =
    1.77        fold_map
    1.78          (fn (name, CodeThingol.Fun info) =>
    1.79 -              map_nsp_fun (name_def false name) >> (fn base => (base, (name, info)))
    1.80 +              map_nsp_fun (name_def false name) >> (fn base => (base, (name, (apsnd o map) fst info)))
    1.81            | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name)
    1.82          ) defs
    1.83        >> (split_list #> apsnd MLFuns);
    1.84 @@ -950,7 +934,7 @@
    1.85               | [info] => MLClass info)));
    1.86      fun mk_inst [(name, CodeThingol.Classinst info)] =
    1.87        map_nsp_fun (name_def false name)
    1.88 -      >> (fn base => ([base], MLClassinst (name, info)));
    1.89 +      >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info)));
    1.90      fun add_group mk defs nsp_nodes =
    1.91        let
    1.92          val names as (name :: names') = map fst defs;
    1.93 @@ -1046,7 +1030,7 @@
    1.94    let
    1.95      val output = case file
    1.96       of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
    1.97 -      | SOME "-" => writeln o code_output
    1.98 +      | SOME "-" => PrintMode.with_default writeln o code_output
    1.99        | SOME file => File.write (Path.explode file) o code_output;
   1.100    in
   1.101      parse_args (Scan.succeed ())
   1.102 @@ -1057,10 +1041,10 @@
   1.103    let
   1.104      val output = case file
   1.105       of NONE => error "OCaml: no internal compilation"
   1.106 -      | SOME "-" => writeln o code_output
   1.107 +      | SOME "-" => PrintMode.with_default writeln o code_output
   1.108        | SOME file => File.write (Path.explode file) o code_output;
   1.109      fun output_file file = File.write (Path.explode file) o code_output;
   1.110 -    val output_diag = writeln o code_output;
   1.111 +    val output_diag = PrintMode.with_default writeln o code_output;
   1.112    in
   1.113      parse_args (Scan.succeed ())
   1.114      #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
   1.115 @@ -1176,7 +1160,7 @@
   1.116      fun pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
   1.117            let
   1.118              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
   1.119 -            fun pr_eq (ts, t) =
   1.120 +            fun pr_eq ((ts, t), _) =
   1.121                let
   1.122                  val consts = map_filter
   1.123                    (fn c => if (is_some o const_syntax) c
   1.124 @@ -1268,21 +1252,12 @@
   1.125        | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
   1.126            let
   1.127              val tyvars = CodeName.intro_vars (map fst vs) init_syms;
   1.128 -            fun pr_instdef (classop, t) =
   1.129 -                let
   1.130 -                  val consts = map_filter
   1.131 -                    (fn c => if (is_some o const_syntax) c
   1.132 -                      then NONE else (SOME o NameSpace.base o deresolv) c)
   1.133 -                      (CodeThingol.fold_constnames (insert (op =)) t []);
   1.134 -                  val vars = init_syms
   1.135 -                    |> CodeName.intro_vars consts;
   1.136 -                in
   1.137 -                  semicolon [
   1.138 -                    (str o classop_name class) classop,
   1.139 -                    str "=",
   1.140 -                    pr_term false vars NOBR t
   1.141 -                  ]
   1.142 -                end;
   1.143 +            fun pr_instdef ((classop, c_inst), _) =
   1.144 +              semicolon [
   1.145 +                (str o classop_name class) classop,
   1.146 +                str "=",
   1.147 +                pr_app false init_syms NOBR (c_inst, [])
   1.148 +              ];
   1.149            in
   1.150              Pretty.block_enclose (
   1.151                Pretty.block [
   1.152 @@ -1401,7 +1376,7 @@
   1.153              val pathname = Path.append destination filename;
   1.154              val _ = File.mkdir (Path.dir pathname);
   1.155            in File.write pathname end
   1.156 -      | write_module NONE _ = writeln;
   1.157 +      | write_module NONE _ = PrintMode.with_default writeln;
   1.158      fun seri_module (modlname', (imports, (defs, _))) =
   1.159        let
   1.160          val imports' =
   1.161 @@ -1469,7 +1444,7 @@
   1.162      |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
   1.163      |> Pretty.chunks2
   1.164      |> code_output
   1.165 -    |> writeln
   1.166 +    |> PrintMode.with_default writeln
   1.167    end;
   1.168  
   1.169  
   1.170 @@ -1627,11 +1602,11 @@
   1.171        reff := NONE;
   1.172        seri (SOME [val_name]) code;
   1.173        use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
   1.174 -        ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");
   1.175 +        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");
   1.176        case !reff
   1.177         of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
   1.178              ^ " (reference probably has been shadowed)")
   1.179 -        | SOME value => value
   1.180 +        | SOME f => f ()
   1.181        );
   1.182    in
   1.183      code