src/Tools/Code/code_preproc.ML
changeset 63157 65a81a4ef7f8
parent 63073 413184c7a2a2
child 63160 80a91e0e236e
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    val chain: T -> T -> T
     1.5    val lift: (Proof.context -> cterm -> (cterm -> thm) * thm) -> T
     1.6    val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv;
     1.7 -  val evaluation: T -> ((term -> term) -> 'a -> 'b) ->
     1.8 +  val computation: T -> ((term -> term) -> 'a -> 'b) ->
     1.9      (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b;
    1.10  end = struct
    1.11  
    1.12 @@ -151,7 +151,7 @@
    1.13      val (postproc, ct') = sandwich ctxt ct;
    1.14    in postproc (conv ctxt (Thm.term_of ct') ct') end;
    1.15  
    1.16 -fun evaluation sandwich lift_postproc eval ctxt t =
    1.17 +fun computation sandwich lift_postproc eval ctxt t =
    1.18    let
    1.19      val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t);
    1.20    in
    1.21 @@ -538,32 +538,45 @@
    1.22  
    1.23  (** retrieval and evaluation interfaces **)
    1.24  
    1.25 +(*
    1.26 +  naming conventions
    1.27 +  * evaluator "eval" is either
    1.28 +    * conversion "conv"
    1.29 +    * value computation "comp"
    1.30 +  * "evaluation" is a lifting of an evaluator
    1.31 +*)
    1.32 +
    1.33  fun obtain ignore_cache ctxt consts ts = apsnd snd
    1.34    (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    1.35      (extend_arities_eqngr ctxt consts ts));
    1.36  
    1.37 -fun dynamic_evaluator eval ctxt t =
    1.38 +fun dynamic_evaluation eval ctxt t =
    1.39    let
    1.40      val consts = fold_aterms
    1.41        (fn Const (c, _) => insert (op =) c | _ => I) t [];
    1.42      val (algebra, eqngr) = obtain false ctxt consts [t];
    1.43    in eval algebra eqngr t end;
    1.44  
    1.45 +fun static_evaluation ctxt consts eval =
    1.46 +  let
    1.47 +    val (algebra, eqngr) = obtain true ctxt consts [];
    1.48 +  in eval { algebra = algebra, eqngr = eqngr } end;
    1.49 +
    1.50  fun dynamic_conv ctxt conv =
    1.51 -  Sandwich.conversion (value_sandwich ctxt) (dynamic_evaluator conv) ctxt;
    1.52 +  Sandwich.conversion (value_sandwich ctxt)
    1.53 +    (dynamic_evaluation conv) ctxt;
    1.54  
    1.55  fun dynamic_value ctxt lift_postproc evaluator =
    1.56 -  Sandwich.evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
    1.57 +  Sandwich.computation (value_sandwich ctxt) lift_postproc
    1.58 +    (dynamic_evaluation evaluator) ctxt;
    1.59  
    1.60  fun static_conv { ctxt, consts } conv =
    1.61 -  let
    1.62 -    val (algebra, eqngr) = obtain true ctxt consts [];
    1.63 -  in Sandwich.conversion (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
    1.64 +  Sandwich.conversion (value_sandwich ctxt)
    1.65 +    (static_evaluation ctxt consts conv);
    1.66  
    1.67 -fun static_value { ctxt, lift_postproc, consts } evaluator =
    1.68 -  let
    1.69 -    val (algebra, eqngr) = obtain true ctxt consts [];
    1.70 -  in Sandwich.evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
    1.71 +fun static_value { ctxt, lift_postproc, consts } comp =
    1.72 +  Sandwich.computation (value_sandwich ctxt) lift_postproc
    1.73 +    (static_evaluation ctxt consts comp);
    1.74  
    1.75  
    1.76  (** setup **)