src/HOL/Tools/code_evaluation.ML
changeset 56973 62da80041afd
parent 56926 aaea99edc040
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu May 15 16:38:31 2014 +0200
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu May 15 16:38:31 2014 +0200
     1.3 @@ -9,11 +9,15 @@
     1.4    val dynamic_value: Proof.context -> term -> term option
     1.5    val dynamic_value_strict: Proof.context -> term -> term
     1.6    val dynamic_value_exn: Proof.context -> term -> term Exn.result
     1.7 -  val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option
     1.8 -  val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term
     1.9 -  val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result
    1.10 +  val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.11 +    -> Proof.context -> term -> term option
    1.12 +  val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.13 +    -> Proof.context -> term -> term
    1.14 +  val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.15 +    -> Proof.context -> term -> term Exn.result
    1.16    val dynamic_conv: Proof.context -> conv
    1.17 -  val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
    1.18 +  val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.19 +    -> Proof.context -> conv
    1.20    val put_term: (unit -> term) -> Proof.context -> Proof.context
    1.21    val tracing: string -> 'a -> 'a
    1.22  end;
    1.23 @@ -160,8 +164,7 @@
    1.24        | NONE => NONE)
    1.25    | subst_termify t = subst_termify_app (strip_comb t) 
    1.26  
    1.27 -fun check_termify ctxt ts =
    1.28 -  the_default ts (map_default subst_termify ts);
    1.29 +fun check_termify _ ts = the_default ts (map_default subst_termify ts);
    1.30  
    1.31  val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
    1.32  
    1.33 @@ -188,10 +191,11 @@
    1.34  val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
    1.35  val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
    1.36  
    1.37 -fun gen_static_value static_value ctxt consts Ts =
    1.38 +fun gen_static_value static_value { ctxt, consts, Ts } =
    1.39    let
    1.40 -    val static_value' = static_value cookie ctxt NONE I
    1.41 -      (union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts)
    1.42 +    val static_value' = static_value cookie
    1.43 +      { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
    1.44 +        union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
    1.45    in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
    1.46  
    1.47  val static_value = gen_static_value Code_Runtime.static_value;
    1.48 @@ -214,13 +218,13 @@
    1.49  fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
    1.50    Code_Runtime.dynamic_holds_conv;
    1.51  
    1.52 -fun static_conv ctxt consts Ts =
    1.53 +fun static_conv { ctxt, consts, Ts }  =
    1.54    let
    1.55      val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
    1.56        map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
    1.57          (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
    1.58 -    val value = static_value ctxt consts Ts;
    1.59 -    val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
    1.60 +    val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts };
    1.61 +    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts };
    1.62    in
    1.63      fn ctxt' => certify_eval ctxt' value holds
    1.64    end;