clarified stylized status of sandwich algebra
authorhaftmann
Thu May 15 16:46:29 2014 +0200 (2014-05-15)
changeset 56976dc01225a2f77
parent 56975 1f3e60572081
child 56977 a33fe940a557
clarified stylized status of sandwich algebra
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:33 2014 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:46:29 2014 +0200
     1.3 @@ -107,27 +107,41 @@
     1.4  
     1.5  (* algebra of sandwiches: cterm transformations with pending postprocessors *)
     1.6  
     1.7 +fun matches_transitive eq1 eq2 = Thm.rhs_of eq1 aconvc Thm.lhs_of eq2;
     1.8 +
     1.9  fun trans_comb eq1 eq2 =
    1.10 -  if Thm.is_reflexive eq1 then eq2
    1.11 -  else if Thm.is_reflexive eq2 then eq1
    1.12 +  (*explicit assertions: evaluation conversion stacks are error-prone*)
    1.13 +  if Thm.is_reflexive eq1 then (@{assert} (matches_transitive eq1 eq2); eq2)
    1.14 +  else if Thm.is_reflexive eq2 then (@{assert} (matches_transitive eq1 eq2); eq1)
    1.15    else Thm.transitive eq1 eq2;
    1.16  
    1.17  fun trans_conv_rule conv eq = trans_comb eq (conv (Thm.rhs_of eq));
    1.18  
    1.19 -type sandwich = Proof.context -> cterm -> (thm -> thm) * cterm;
    1.20 -type conv_sandwich = Proof.context -> cterm -> conv * thm;
    1.21 +structure Sandwich : sig
    1.22 +  type T = Proof.context -> cterm -> (thm -> thm) * cterm;
    1.23 +  val chain: T -> T -> T
    1.24 +  val lift: (Proof.context -> cterm -> (cterm -> thm) * thm) -> T
    1.25 +  val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv;
    1.26 +  val evaluation: T -> ((term -> term) -> 'a -> 'b) ->
    1.27 +    (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b;
    1.28 +end = struct
    1.29 +
    1.30 +type T = Proof.context -> cterm -> (thm -> thm) * cterm;
    1.31  
    1.32  fun chain sandwich2 sandwich1 ctxt =
    1.33    sandwich1 ctxt
    1.34    ##>> sandwich2 ctxt
    1.35    #>> (op o);
    1.36  
    1.37 -fun lift_conv_sandwich conv_sandwhich ctxt ct =
    1.38 +fun lift conv_sandwhich ctxt ct =
    1.39    let
    1.40      val (postproc_conv, eq) = conv_sandwhich ctxt ct;
    1.41 -  in (trans_conv_rule postproc_conv o trans_comb eq, Thm.rhs_of eq) end;
    1.42 +    fun potentail_trans_comb eq1 eq2 =
    1.43 +      if matches_transitive eq1 eq2 then trans_comb eq1 eq2 else eq2;
    1.44 +        (*weakened protocol for plain term evaluation*)
    1.45 +  in (trans_conv_rule postproc_conv o potentail_trans_comb eq, Thm.rhs_of eq) end;
    1.46  
    1.47 -fun finalize sandwich conv ctxt ct =
    1.48 +fun conversion sandwich conv ctxt ct =
    1.49    let
    1.50      val (postproc, ct') = sandwich ctxt ct;
    1.51    in postproc (conv ctxt (term_of ct') ct') end;
    1.52 @@ -142,6 +156,8 @@
    1.53      |> lift_postproc (term_of o Thm.rhs_of o postproc o Thm.reflexive o cert)
    1.54    end;
    1.55  
    1.56 +end;
    1.57 +
    1.58  
    1.59  (* post- and preprocessing *)
    1.60  
    1.61 @@ -190,12 +206,12 @@
    1.62        #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'))
    1.63    in fn ctxt' => pre_conv ctxt' #> pair (post_conv ctxt') end;
    1.64  
    1.65 -fun simplifier_sandwich ctxt = lift_conv_sandwich (simplifier_conv_sandwich ctxt);
    1.66 +fun simplifier_sandwich ctxt = Sandwich.lift (simplifier_conv_sandwich ctxt);
    1.67  
    1.68  fun value_sandwich ctxt =
    1.69    normalized_tfrees_sandwich
    1.70 -  |> chain no_variables_sandwich
    1.71 -  |> chain (simplifier_sandwich ctxt);
    1.72 +  |> Sandwich.chain no_variables_sandwich
    1.73 +  |> Sandwich.chain (simplifier_sandwich ctxt);
    1.74  
    1.75  fun print_codeproc ctxt =
    1.76    let
    1.77 @@ -493,20 +509,20 @@
    1.78    in eval algebra eqngr t end;
    1.79  
    1.80  fun dynamic_conv ctxt conv =
    1.81 -  finalize (value_sandwich ctxt) (dynamic_evaluator conv) ctxt;
    1.82 +  Sandwich.conversion (value_sandwich ctxt) (dynamic_evaluator conv) ctxt;
    1.83  
    1.84  fun dynamic_value ctxt lift_postproc evaluator =
    1.85 -  evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
    1.86 +  Sandwich.evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
    1.87  
    1.88  fun static_conv { ctxt, consts } conv =
    1.89    let
    1.90      val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
    1.91 -  in finalize (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
    1.92 +  in Sandwich.conversion (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
    1.93  
    1.94  fun static_value { ctxt, lift_postproc, consts } evaluator =
    1.95    let
    1.96      val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
    1.97 -  in evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
    1.98 +  in Sandwich.evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
    1.99  
   1.100  
   1.101  (** setup **)