clarified names of variants
authorhaftmann
Thu May 26 15:27:50 2016 +0200 (2016-05-26)
changeset 631563cb84e4469a7
parent 63155 ea8540c71581
child 63157 65a81a4ef7f8
clarified names of variants
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 09:05:00 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4        o reject_vars ctxt;
     1.5  
     1.6  fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
     1.7 -  Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
     1.8 +  Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
     1.9      K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    1.10  
    1.11  end; (*local*)
     2.1 --- a/src/Tools/Code/code_simp.ML	Thu May 26 09:05:00 2016 +0200
     2.2 +++ b/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
     2.3 @@ -94,7 +94,7 @@
     2.4  (* evaluation with static code context *)
     2.5  
     2.6  fun static_conv { ctxt, simpset, consts } =
     2.7 -  Code_Thingol.static_conv_simple { ctxt = ctxt, consts = consts }
     2.8 +  Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
     2.9      (K oo rewrite_modulo ctxt simpset);
    2.10  
    2.11  fun static_tac { ctxt, simpset, consts } =
     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 26 09:05:00 2016 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     3.3 @@ -91,11 +91,11 @@
     3.4    val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     3.5      -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     3.6      -> term -> 'a
     3.7 -  val static_conv: { ctxt: Proof.context, consts: string list }
     3.8 +  val static_conv_thingol: { ctxt: Proof.context, consts: string list }
     3.9      -> ({ program: program, deps: string list }
    3.10        -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
    3.11      -> Proof.context -> conv
    3.12 -  val static_conv_simple: { ctxt: Proof.context, consts: string list }
    3.13 +  val static_conv_isa: { ctxt: Proof.context, consts: string list }
    3.14      -> (program -> Proof.context -> term -> conv)
    3.15      -> Proof.context -> conv
    3.16    val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list }
    3.17 @@ -857,7 +857,7 @@
    3.18        ensure_value ctxt algebra eqngr t ([], program);
    3.19    in subevaluator ctxt t (vs_ty', t') deps end;
    3.20  
    3.21 -fun static_evaluator ctxt evaluator consts { algebra, eqngr } =
    3.22 +fun static_evaluator_thingol ctxt evaluator consts { algebra, eqngr } =
    3.23    let
    3.24      fun generate_consts ctxt algebra eqngr =
    3.25        fold_map (ensure_const ctxt algebra eqngr false);
    3.26 @@ -866,7 +866,7 @@
    3.27      val subevaluator = evaluator { program = program, deps = deps };
    3.28    in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
    3.29  
    3.30 -fun static_evaluator_simple ctxt evaluator consts { algebra, eqngr } =
    3.31 +fun static_evaluator_isa ctxt evaluator consts { algebra, eqngr } =
    3.32    let
    3.33      fun generate_consts ctxt algebra eqngr =
    3.34        fold_map (ensure_const ctxt algebra eqngr false);
    3.35 @@ -874,14 +874,14 @@
    3.36        invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    3.37    in evaluator (program: program) end;
    3.38  
    3.39 -fun static_conv (ctxt_consts as { ctxt, consts }) conv =
    3.40 -  Code_Preproc.static_conv ctxt_consts (static_evaluator ctxt (K oo conv) consts);
    3.41 +fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
    3.42 +  Code_Preproc.static_conv ctxt_consts (static_evaluator_thingol ctxt (K oo conv) consts);
    3.43  
    3.44 -fun static_conv_simple (ctxt_consts as { ctxt, consts }) conv =
    3.45 -  Code_Preproc.static_conv ctxt_consts (static_evaluator_simple ctxt conv consts);
    3.46 +fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
    3.47 +  Code_Preproc.static_conv ctxt_consts (static_evaluator_isa ctxt conv consts);
    3.48  
    3.49  fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
    3.50 -  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator ctxt evaluator consts);
    3.51 +  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator_thingol ctxt evaluator consts);
    3.52  
    3.53  
    3.54  (** constant expressions **)
     4.1 --- a/src/Tools/nbe.ML	Thu May 26 09:05:00 2016 +0200
     4.2 +++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
     4.3 @@ -604,7 +604,7 @@
     4.4  
     4.5  fun static_conv (ctxt_consts as { ctxt, ... }) =
     4.6    let
     4.7 -    val evaluator = Code_Thingol.static_conv ctxt_consts
     4.8 +    val evaluator = Code_Thingol.static_conv_thingol ctxt_consts
     4.9        (fn { program, ... } => oracle (compile true ctxt program));
    4.10    in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
    4.11