src/Tools/Code/code_runtime.ML
changeset 63160 80a91e0e236e
parent 63159 84c6dd947b75
child 63163 b561284a4214
     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 @@ -28,15 +28,15 @@
     1.4      -> Proof.context -> term -> 'a Exn.result
     1.5    val dynamic_holds_conv: Proof.context -> conv
     1.6    val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
     1.7 -  val static_value': (Proof.context -> term -> 'a) cookie
     1.8 +  val fully_static_value: (Proof.context -> term -> 'a) cookie
     1.9      -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
    1.10             consts: (string * typ) list, T: typ }
    1.11      -> Proof.context -> term -> 'a option (*EXPERIMENTAL!*)
    1.12 -  val static_value_strict': (Proof.context -> term -> 'a) cookie
    1.13 +  val fully_static_value_strict: (Proof.context -> term -> 'a) cookie
    1.14      -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
    1.15             consts: (string * typ) list, T: typ }
    1.16      -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
    1.17 -  val static_value_exn': (Proof.context -> term -> 'a) cookie
    1.18 +  val fully_static_value_exn: (Proof.context -> term -> 'a) cookie
    1.19      -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
    1.20             consts: (string * typ) list, T: typ }
    1.21      -> Proof.context -> term -> 'a Exn.result (*EXPERIMENTAL!*)
    1.22 @@ -201,7 +201,7 @@
    1.23  end; (*local*)
    1.24  
    1.25  
    1.26 -(** full static evaluation -- still with limited coverage! **)
    1.27 +(** fully static evaluation -- still with limited coverage! **)
    1.28  
    1.29  fun evaluation_code ctxt module_name program tycos consts =
    1.30    let
    1.31 @@ -293,7 +293,7 @@
    1.32        ml_name_for_typ = ml_name_for_typ } Ts
    1.33    end;
    1.34  
    1.35 -fun compile_evaluator cookie ctxt cs_code cTs T { program, deps } =
    1.36 +fun compile_computation cookie ctxt cs_code cTs T { program, deps } =
    1.37    let
    1.38      val (context_code, (_, const_map)) =
    1.39        evaluation_code ctxt structure_generated program [] cs_code;
    1.40 @@ -302,21 +302,21 @@
    1.41      val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names);
    1.42    in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end;
    1.43  
    1.44 -fun static_value_exn' cookie { ctxt, lift_postproc, consts, T } =
    1.45 +fun fully_static_value_exn cookie { ctxt, lift_postproc, consts, T } =
    1.46    let
    1.47      val thy = Proof_Context.theory_of ctxt;
    1.48      val cs_code = map (Axclass.unoverload_const thy) consts;
    1.49      val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code;
    1.50 -    val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    1.51 +    val computation = Code_Thingol.static_value { ctxt = ctxt,
    1.52        lift_postproc = Exn.map_res o lift_postproc, consts = cs_code }
    1.53 -      (compile_evaluator cookie ctxt cs_code cTs T);
    1.54 +      (compile_computation cookie ctxt cs_code cTs T);
    1.55    in fn ctxt' =>
    1.56 -    evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
    1.57 +    computation ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
    1.58    end;
    1.59  
    1.60 -fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
    1.61 +fun fully_static_value_strict cookie = Exn.release ooo fully_static_value_exn cookie;
    1.62  
    1.63 -fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
    1.64 +fun fully_static_value cookie = partiality_as_none ooo fully_static_value_exn cookie;
    1.65  
    1.66  
    1.67  (** code antiquotation **)