src/Tools/Code/code_runtime.ML
author haftmann
Wed Sep 15 16:56:31 2010 +0200 (2010-09-15)
changeset 39422 9019b6afaa4a
parent 39404 a8c337299bc1
child 39473 33638f4883ac
permissions -rw-r--r--
proper interface for code_reflect
     1 (*  Title:      Tools/Code/code_runtime.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Runtime services building on code generation into implementation language SML.
     5 *)
     6 
     7 signature CODE_RUNTIME =
     8 sig
     9   val target: string
    10   val value: string option
    11     -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    12     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    13   val code_reflect: (string * string list) list -> string list -> string -> string option
    14     -> theory -> theory
    15   val setup: theory -> theory
    16 end;
    17 
    18 structure Code_Runtime : CODE_RUNTIME =
    19 struct
    20 
    21 (** evaluation **)
    22 
    23 val target = "Eval";
    24 
    25 val truth_struct = "Code_Truth";
    26 
    27 fun value some_target cookie postproc thy t args =
    28   let
    29     val ctxt = ProofContext.init_global thy;
    30     fun evaluator naming program ((_, (_, ty)), t) deps =
    31       let
    32         val _ = if Code_Thingol.contains_dictvar t then
    33           error "Term to be evaluated contains free dictionaries" else ();
    34         val value_name = "Value.VALUE.value"
    35         val program' = program
    36           |> Graph.new_node (value_name,
    37               Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    38           |> fold (curry Graph.add_edge value_name) deps;
    39         val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    40           (the_default target some_target) NONE "Code" [] naming program' [value_name];
    41         val value_code = space_implode " "
    42           (value_name' :: map (enclose "(" ")") args);
    43       in ML_Context.value ctxt cookie (program_code, value_code) end;
    44   in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    45 
    46 
    47 (** instrumentalization **)
    48 
    49 fun evaluation_code thy module_name tycos consts =
    50   let
    51     val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    52     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    53     val (ml_code, target_names) = Code_Target.produce_code_for thy
    54       target NONE module_name [] naming program (consts' @ tycos');
    55     val (consts'', tycos'') = chop (length consts') target_names;
    56     val consts_map = map2 (fn const => fn NONE =>
    57         error ("Constant " ^ (quote o Code.string_of_const thy) const
    58           ^ "\nhas a user-defined serialization")
    59       | SOME const'' => (const, const'')) consts consts''
    60     val tycos_map = map2 (fn tyco => fn NONE =>
    61         error ("Type " ^ (quote o Sign.extern_type thy) tyco
    62           ^ "\nhas a user-defined serialization")
    63       | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    64   in (ml_code, (tycos_map, consts_map)) end;
    65 
    66 
    67 (* by antiquotation *)
    68 
    69 local
    70 
    71 structure Code_Antiq_Data = Proof_Data
    72 (
    73   type T = (string list * string list) * (bool
    74     * (string * ((string * string) list * (string * string) list)) lazy);
    75   fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
    76 );
    77 
    78 val is_first_occ = fst o snd o Code_Antiq_Data.get;
    79 
    80 fun register_code new_tycos new_consts ctxt =
    81   let
    82     val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
    83     val tycos' = fold (insert (op =)) new_tycos tycos;
    84     val consts' = fold (insert (op =)) new_consts consts;
    85     val acc_code = Lazy.lazy (fn () =>
    86       evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
    87   in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
    88 
    89 fun register_const const = register_code [] [const];
    90 
    91 fun register_datatype tyco constrs = register_code [tyco] constrs;
    92 
    93 fun print_const const all_struct_name tycos_map consts_map =
    94   (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
    95 
    96 fun print_code is_first print_it ctxt =
    97   let
    98     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
    99     val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
   100     val ml_code = if is_first then ml_code
   101       else "";
   102     val all_struct_name = "Isabelle";
   103   in (ml_code, print_it all_struct_name tycos_map consts_map) end;
   104 
   105 in
   106 
   107 fun ml_code_antiq raw_const background =
   108   let
   109     val const = Code.check_const (ProofContext.theory_of background) raw_const;
   110     val is_first = is_first_occ background;
   111     val background' = register_const const background;
   112   in (print_code is_first (print_const const), background') end;
   113 
   114 end; (*local*)
   115 
   116 
   117 (* reflection support *)
   118 
   119 fun check_datatype thy tyco consts =
   120   let
   121     val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
   122     val missing_constrs = subtract (op =) consts constrs;
   123     val _ = if null missing_constrs then []
   124       else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
   125         ^ " for datatype " ^ quote tyco);
   126     val false_constrs = subtract (op =) constrs consts;
   127     val _ = if null false_constrs then []
   128       else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
   129         ^ " for datatype " ^ quote tyco);
   130   in () end;
   131 
   132 fun add_eval_tyco (tyco, tyco') thy =
   133   let
   134     val k = Sign.arity_number thy tyco;
   135     fun pr pr' fxy [] = tyco'
   136       | pr pr' fxy [ty] =
   137           Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
   138       | pr pr' fxy tys =
   139           Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   140   in
   141     thy
   142     |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
   143   end;
   144 
   145 fun add_eval_constr (const, const') thy =
   146   let
   147     val k = Code.args_number thy const;
   148     fun pr pr' fxy ts = Code_Printer.brackify fxy
   149       (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
   150   in
   151     thy
   152     |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
   153   end;
   154 
   155 fun add_eval_const (const, const') = Code_Target.add_const_syntax target
   156   const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
   157 
   158 fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
   159       thy
   160       |> Code_Target.add_reserved target module_name
   161       |> Context.theory_map
   162         (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
   163       |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
   164       |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
   165       |> fold (add_eval_const o apsnd Code_Printer.str) const_map
   166   | process (code_body, _) _ (SOME file_name) thy =
   167       let
   168         val preamble =
   169           "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
   170           ^ "; DO NOT EDIT! *)";
   171         val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
   172       in
   173         thy
   174       end;
   175 
   176 fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
   177   let
   178     val datatypes = map (fn (raw_tyco, raw_cos) =>
   179       (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
   180     val _ = map (uncurry (check_datatype thy)) datatypes;
   181     val tycos = map fst datatypes;
   182     val constrs = maps snd datatypes;
   183     val functions = map (prep_const thy) raw_functions;
   184     val result = evaluation_code thy module_name tycos (constrs @ functions)
   185       |> (apsnd o apsnd) (chop (length constrs));
   186   in
   187     thy
   188     |> process result module_name some_file
   189   end;
   190 
   191 val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
   192 val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
   193 
   194 
   195 (** Isar setup **)
   196 
   197 val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
   198 
   199 local
   200 
   201 val datatypesK = "datatypes";
   202 val functionsK = "functions";
   203 val fileK = "file";
   204 val andK = "and"
   205 
   206 val _ = List.app Keyword.keyword [datatypesK, functionsK];
   207 
   208 val parse_datatype =
   209   Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
   210 
   211 in
   212 
   213 val _ =
   214   Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
   215     Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
   216       ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
   217     -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
   218     -- Scan.option (Parse.$$$ fileK |-- Parse.name)
   219   >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
   220     (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
   221 
   222 end; (*local*)
   223 
   224 val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
   225 
   226 end; (*struct*)