src/Tools/Code/code_runtime.ML
changeset 55147 bce3dbc11f95
parent 53171 a5e54d4d9081
child 55150 0940309ed8f1
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  datatype truth = Holds;
     1.5  
     1.6  val _ = Theory.setup
     1.7 -  (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
     1.8 +  (Code_Target.extend_target (target, (Code_ML.target_SML, I))
     1.9    #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
    1.10      [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
    1.11    #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
    1.12 @@ -87,10 +87,13 @@
    1.13      val ctxt = Proof_Context.init_global thy;
    1.14    in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
    1.15  
    1.16 -fun obtain_evaluator thy some_target naming program consts expr =
    1.17 -  Code_Target.evaluator thy (the_default target some_target) naming program consts expr
    1.18 +fun obtain_evaluator thy some_target program consts expr =
    1.19 +  Code_Target.evaluator thy (the_default target some_target) program consts expr
    1.20    |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    1.21  
    1.22 +fun obtain_evaluator' thy some_target program =
    1.23 +  obtain_evaluator thy some_target program o map Code_Symbol.Constant;
    1.24 +
    1.25  fun evaluation cookie thy evaluator vs_t args =
    1.26    let
    1.27      val ctxt = Proof_Context.init_global thy;
    1.28 @@ -110,8 +113,8 @@
    1.29      val _ = if ! trace
    1.30        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
    1.31        else ()
    1.32 -    fun evaluator naming program ((_, vs_ty), t) deps =
    1.33 -      evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
    1.34 +    fun evaluator program ((_, vs_ty), t) deps =
    1.35 +      evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
    1.36    in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
    1.37  
    1.38  fun dynamic_value_strict cookie thy some_target postproc t args =
    1.39 @@ -120,9 +123,9 @@
    1.40  fun dynamic_value cookie thy some_target postproc t args =
    1.41    partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
    1.42  
    1.43 -fun static_evaluator cookie thy some_target naming program consts' =
    1.44 +fun static_evaluator cookie thy some_target program consts' =
    1.45    let
    1.46 -    val evaluator = obtain_evaluator thy some_target naming program consts'
    1.47 +    val evaluator = obtain_evaluator' thy some_target program consts'
    1.48    in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
    1.49  
    1.50  fun static_value_exn cookie thy some_target postproc consts =
    1.51 @@ -175,13 +178,13 @@
    1.52  in
    1.53  
    1.54  fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
    1.55 -  (fn naming => fn program => fn vs_t => fn deps =>
    1.56 -    check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
    1.57 +  (fn program => fn vs_t => fn deps =>
    1.58 +    check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
    1.59        o reject_vars thy;
    1.60  
    1.61  fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
    1.62 -  (fn naming => fn program => fn consts' =>
    1.63 -    check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
    1.64 +  (fn program => fn consts' =>
    1.65 +    check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
    1.66        o reject_vars thy;
    1.67  
    1.68  end; (*local*)
    1.69 @@ -192,23 +195,22 @@
    1.70  fun evaluation_code thy module_name tycos consts =
    1.71    let
    1.72      val ctxt = Proof_Context.init_global thy;
    1.73 -    val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    1.74 -    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    1.75 +    val program = Code_Thingol.consts_program thy false consts;
    1.76      val (ml_modules, target_names) =
    1.77        Code_Target.produce_code_for thy
    1.78 -        target NONE module_name [] naming program (consts' @ tycos');
    1.79 +        target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
    1.80      val ml_code = space_implode "\n\n" (map snd ml_modules);
    1.81 -    val (consts'', tycos'') = chop (length consts') target_names;
    1.82 +    val (consts', tycos') = chop (length consts) target_names;
    1.83      val consts_map = map2 (fn const =>
    1.84        fn NONE =>
    1.85            error ("Constant " ^ (quote o Code.string_of_const thy) const ^
    1.86              "\nhas a user-defined serialization")
    1.87 -       | SOME const'' => (const, const'')) consts consts''
    1.88 +       | SOME const' => (const, const')) consts consts'
    1.89      val tycos_map = map2 (fn tyco =>
    1.90        fn NONE =>
    1.91            error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
    1.92              "\nhas a user-defined serialization")
    1.93 -        | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    1.94 +        | SOME tyco' => (tyco, tyco')) tycos tycos';
    1.95    in (ml_code, (tycos_map, consts_map)) end;
    1.96  
    1.97