src/Tools/Code/code_runtime.ML
changeset 39404 a8c337299bc1
parent 39401 887f4218a39a
child 39422 9019b6afaa4a
equal deleted inserted replaced
39403:aad9f3cfa1d9 39404:a8c337299bc1
     5 *)
     5 *)
     6 
     6 
     7 signature CODE_RUNTIME =
     7 signature CODE_RUNTIME =
     8 sig
     8 sig
     9   val target: string
     9   val target: string
    10   val eval: string option
    10   val value: string option
    11     -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    11     -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    12     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    12     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    13   val setup: theory -> theory
    13   val setup: theory -> theory
    14 end;
    14 end;
    15 
    15 
    16 structure Code_Runtime : CODE_RUNTIME =
    16 structure Code_Runtime : CODE_RUNTIME =
    17 struct
    17 struct
    18 
    18 
    19 (** generic **)
    19 (** evaluation **)
    20 
    20 
    21 val target = "Eval";
    21 val target = "Eval";
    22 
    22 
    23 fun evaluation_code thy module_name tycos consts =
    23 fun value some_target cookie postproc thy t args =
    24   let
       
    25     val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
       
    26     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
       
    27     val (ml_code, target_names) = Code_Target.produce_code_for thy
       
    28       target NONE module_name [] naming program (consts' @ tycos');
       
    29     val (consts'', tycos'') = chop (length consts') target_names;
       
    30     val consts_map = map2 (fn const => fn NONE =>
       
    31         error ("Constant " ^ (quote o Code.string_of_const thy) const
       
    32           ^ "\nhas a user-defined serialization")
       
    33       | SOME const'' => (const, const'')) consts consts''
       
    34     val tycos_map = map2 (fn tyco => fn NONE =>
       
    35         error ("Type " ^ (quote o Sign.extern_type thy) tyco
       
    36           ^ "\nhas a user-defined serialization")
       
    37       | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
       
    38   in (ml_code, (tycos_map, consts_map)) end;
       
    39 
       
    40 
       
    41 (** evaluation **)
       
    42 
       
    43 fun eval some_target cookie postproc thy t args =
       
    44   let
    24   let
    45     val ctxt = ProofContext.init_global thy;
    25     val ctxt = ProofContext.init_global thy;
    46     fun evaluator naming program ((_, (_, ty)), t) deps =
    26     fun evaluator naming program ((_, (_, ty)), t) deps =
    47       let
    27       let
    48         val _ = if Code_Thingol.contains_dictvar t then
    28         val _ = if Code_Thingol.contains_dictvar t then
    58           (value_name' :: map (enclose "(" ")") args);
    38           (value_name' :: map (enclose "(" ")") args);
    59       in ML_Context.value ctxt cookie (program_code, value_code) end;
    39       in ML_Context.value ctxt cookie (program_code, value_code) end;
    60   in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    40   in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    61 
    41 
    62 
    42 
    63 (** instrumentalization by antiquotation **)
    43 (** instrumentalization **)
       
    44 
       
    45 fun evaluation_code thy module_name tycos consts =
       
    46   let
       
    47     val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
       
    48     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
       
    49     val (ml_code, target_names) = Code_Target.produce_code_for thy
       
    50       target NONE module_name [] naming program (consts' @ tycos');
       
    51     val (consts'', tycos'') = chop (length consts') target_names;
       
    52     val consts_map = map2 (fn const => fn NONE =>
       
    53         error ("Constant " ^ (quote o Code.string_of_const thy) const
       
    54           ^ "\nhas a user-defined serialization")
       
    55       | SOME const'' => (const, const'')) consts consts''
       
    56     val tycos_map = map2 (fn tyco => fn NONE =>
       
    57         error ("Type " ^ (quote o Sign.extern_type thy) tyco
       
    58           ^ "\nhas a user-defined serialization")
       
    59       | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
       
    60   in (ml_code, (tycos_map, consts_map)) end;
       
    61 
       
    62 
       
    63 (* by antiquotation *)
    64 
    64 
    65 local
    65 local
    66 
    66 
    67 structure Code_Antiq_Data = Proof_Data
    67 structure Code_Antiq_Data = Proof_Data
    68 (
    68 (
   108   in (print_code is_first (print_const const), background') end;
   108   in (print_code is_first (print_const const), background') end;
   109 
   109 
   110 end; (*local*)
   110 end; (*local*)
   111 
   111 
   112 
   112 
   113 (** reflection support **)
   113 (* reflection support *)
   114 
   114 
   115 fun check_datatype thy tyco consts =
   115 fun check_datatype thy tyco consts =
   116   let
   116   let
   117     val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
   117     val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
   118     val missing_constrs = subtract (op =) consts constrs;
   118     val missing_constrs = subtract (op =) consts constrs;