clarified proof context vs. background theory
authorhaftmann
Thu May 26 15:27:50 2016 +0200 (2016-05-26)
changeset 6315984c6dd947b75
parent 63158 534f16b0ca39
child 63160 80a91e0e236e
clarified proof context vs. background theory
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4      val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
     1.5      val tycos' = fold (insert (op =)) new_tycos tycos;
     1.6      val consts' = fold (insert (op =)) new_consts consts;
     1.7 -    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts';
     1.8 +    val program = Code_Thingol.consts_program ctxt consts';
     1.9      val acc_code = Lazy.lazy (fn () =>
    1.10        evaluation_code ctxt structure_generated program tycos' consts'
    1.11        |> apsnd snd);
    1.12 @@ -440,7 +440,7 @@
    1.13        |> apsnd flat;
    1.14      val functions = map (prep_const thy) raw_functions;
    1.15      val consts = constrs @ functions;
    1.16 -    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts;
    1.17 +    val program = Code_Thingol.consts_program ctxt consts;
    1.18      val result = evaluation_code ctxt module_name program tycos consts
    1.19        |> (apsnd o apsnd) (chop (length constrs));
    1.20    in
     2.1 --- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     2.3 @@ -429,8 +429,7 @@
     2.4  
     2.5  fun export_code ctxt all_public cs seris =
     2.6    let
     2.7 -    val thy = Proof_Context.theory_of ctxt;
     2.8 -    val program = Code_Thingol.consts_program thy cs;
     2.9 +    val program = Code_Thingol.consts_program ctxt cs;
    2.10      val _ = map (fn (((target_name, module_name), some_path), args) =>
    2.11        export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
    2.12    in () end;
    2.13 @@ -442,20 +441,17 @@
    2.14  
    2.15  fun produce_code ctxt all_public cs target_name some_width some_module_name args =
    2.16    let
    2.17 -    val thy = Proof_Context.theory_of ctxt;
    2.18 -    val program = Code_Thingol.consts_program thy cs;
    2.19 +    val program = Code_Thingol.consts_program ctxt cs;
    2.20    in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end;
    2.21  
    2.22  fun present_code ctxt cs syms target_name some_width some_module_name args =
    2.23    let
    2.24 -    val thy = Proof_Context.theory_of ctxt;
    2.25 -    val program = Code_Thingol.consts_program thy cs;
    2.26 +    val program = Code_Thingol.consts_program ctxt cs;
    2.27    in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end;
    2.28  
    2.29  fun check_code ctxt all_public cs seris =
    2.30    let
    2.31 -    val thy = Proof_Context.theory_of ctxt;
    2.32 -    val program = Code_Thingol.consts_program thy cs;
    2.33 +    val program = Code_Thingol.consts_program ctxt cs;
    2.34      val _ = map (fn ((target_name, strict), args) =>
    2.35        check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris;
    2.36    in () end;
     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     3.3 @@ -84,7 +84,7 @@
     3.4        * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
     3.5  
     3.6    val read_const_exprs: Proof.context -> string list -> string list
     3.7 -  val consts_program: theory -> string list -> program
     3.8 +  val consts_program: Proof.context -> string list -> program
     3.9    val dynamic_conv: Proof.context -> (program
    3.10      -> typscheme * iterm -> Code_Symbol.T list -> conv)
    3.11      -> conv
    3.12 @@ -776,22 +776,23 @@
    3.13    val empty = Code_Symbol.Graph.empty;
    3.14  );
    3.15  
    3.16 -fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
    3.17 -  Program.change_yield (if ignore_cache then NONE else SOME thy)
    3.18 +fun invoke_generation ignore_cache ctxt (algebra, eqngr) generate thing =
    3.19 +  Program.change_yield
    3.20 +    (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    3.21      (fn program => ([], program)
    3.22 -      |> generate (Proof_Context.init_global thy) algebra eqngr thing
    3.23 +      |> generate ctxt algebra eqngr thing
    3.24        |-> (fn thing => fn (_, program) => (thing, program)));
    3.25  
    3.26  
    3.27  (* program generation *)
    3.28  
    3.29 -fun consts_program_internal thy permissive consts =
    3.30 +fun consts_program_internal ctxt permissive consts =
    3.31    let
    3.32      fun generate_consts ctxt algebra eqngr =
    3.33        fold_map (ensure_const ctxt algebra eqngr permissive);
    3.34    in
    3.35 -    invoke_generation permissive thy
    3.36 -      (Code_Preproc.obtain false (Proof_Context.init_global thy) consts [])
    3.37 +    invoke_generation permissive ctxt
    3.38 +      (Code_Preproc.obtain false ctxt consts [])
    3.39        generate_consts consts
    3.40      |> snd
    3.41    end;
    3.42 @@ -842,7 +843,7 @@
    3.43  fun dynamic_evaluation eval ctxt algebra eqngr t =
    3.44    let
    3.45      val ((program, (vs_ty_t', deps)), _) =
    3.46 -      invoke_generation false (Proof_Context.theory_of ctxt)
    3.47 +      invoke_generation false ctxt
    3.48          (algebra, eqngr) ensure_value t;
    3.49    in eval program t vs_ty_t' deps end;
    3.50  
    3.51 @@ -859,7 +860,7 @@
    3.52      fun generate_consts ctxt algebra eqngr =
    3.53        fold_map (ensure_const ctxt algebra eqngr false);
    3.54      val (deps, program) =
    3.55 -      invoke_generation true (Proof_Context.theory_of ctxt)
    3.56 +      invoke_generation true ctxt
    3.57          (algebra, eqngr) generate_consts consts;
    3.58    in static_eval { program = program, deps = deps } end;
    3.59  
    3.60 @@ -919,9 +920,10 @@
    3.61  
    3.62  fun read_const_exprs ctxt const_exprs =
    3.63    let
    3.64 -    val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
    3.65 +    val (consts, consts_permissive) =
    3.66 +      read_const_exprs_internal ctxt const_exprs;
    3.67      val consts' = implemented_deps
    3.68 -      (consts_program_permissive (Proof_Context.theory_of ctxt) consts_permissive);
    3.69 +      (consts_program_permissive ctxt consts_permissive);
    3.70    in union (op =) consts' consts end;
    3.71  
    3.72