src/Tools/Code/code_runtime.ML
changeset 64995 a7af4045f873
parent 64993 4fb84597ec5a
child 65005 3278831c226d
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:38 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Feb 07 22:15:03 2017 +0100
     1.3 @@ -386,12 +386,15 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun preprocess_conv ctxt = 
     1.8 -  Raw_Simplifier.rewrite ctxt false (get ctxt);
     1.9 +fun preprocess_conv { ctxt } = 
    1.10 +  let
    1.11 +    val rules = get ctxt;
    1.12 +  in fn ctxt' => Raw_Simplifier.rewrite ctxt' false rules end;
    1.13  
    1.14 -fun preprocess_term ctxt =
    1.15 -  Pattern.rewrite_term (Proof_Context.theory_of ctxt)
    1.16 -    (map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt)) [];
    1.17 +fun preprocess_term { ctxt } =
    1.18 +  let
    1.19 +    val rules = map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt);
    1.20 +  in fn ctxt' => Pattern.rewrite_term (Proof_Context.theory_of ctxt') rules [] end;
    1.21  
    1.22  val _ = Theory.setup
    1.23    (Attrib.setup @{binding code_computation_unfold}
    1.24 @@ -419,20 +422,22 @@
    1.25  
    1.26  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    1.27    let
    1.28 +    val preprocess = preprocess_term { ctxt = ctxt };
    1.29      val computation = prechecked_computation T (Code_Preproc.static_value
    1.30        { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.31        (K (checked_computation cTs raw_computation)));
    1.32 -  in fn ctxt' => preprocess_term ctxt' #> computation ctxt' end;
    1.33 +  in fn ctxt' => preprocess ctxt' #> computation ctxt' end;
    1.34  
    1.35  fun mount_computation_conv ctxt cTs T raw_computation conv =
    1.36    let
    1.37 +    val preprocess = preprocess_conv { ctxt = ctxt };
    1.38      val computation_conv = prechecked_conv T (Code_Preproc.static_conv
    1.39        { ctxt = ctxt, consts = [] }
    1.40        (K (fn ctxt' => fn t =>
    1.41          case checked_computation cTs raw_computation ctxt' t of
    1.42            SOME x => conv x
    1.43          | NONE => Conv.all_conv)));
    1.44 -  in fn ctxt' => preprocess_conv ctxt' then_conv computation_conv ctxt' end;
    1.45 +  in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end;
    1.46  
    1.47  local
    1.48  
    1.49 @@ -564,7 +569,7 @@
    1.50        let
    1.51          val evals = Abs ("eval", map snd computation_cTs' --->
    1.52            TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs'))
    1.53 -          |> preprocess_term ctxt
    1.54 +          |> preprocess_term { ctxt = ctxt } ctxt
    1.55        in Code_Thingol.dynamic_value ctxt
    1.56          (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals
    1.57        end;