unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches
authorhaftmann
Thu May 15 16:38:28 2014 +0200 (2014-05-15)
changeset 56968d2b1d95eb722
parent 56967 c3746e999805
child 56969 7491932da574
unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:17 2014 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:28 2014 +0200
     1.3 @@ -24,14 +24,14 @@
     1.4    val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
     1.5    val dynamic_conv: Proof.context
     1.6      -> (code_algebra -> code_graph -> term -> conv) -> conv
     1.7 -  val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a)
     1.8 -    -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'a
     1.9 +  val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b)
    1.10 +    -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'b
    1.11    val static_conv: Proof.context -> string list
    1.12      -> (code_algebra -> code_graph -> Proof.context -> term -> conv)
    1.13      -> Proof.context -> conv
    1.14 -  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list
    1.15 +  val static_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> string list
    1.16      -> (code_algebra -> code_graph -> Proof.context -> term -> 'a)
    1.17 -    -> Proof.context -> term -> 'a
    1.18 +    -> Proof.context -> term -> 'b
    1.19  
    1.20    val setup: theory -> theory
    1.21  end
    1.22 @@ -107,26 +107,47 @@
    1.23    (delete_force "function transformer" name);
    1.24  
    1.25  
    1.26 +(* algebra of sandwiches: cterm transformations with pending postprocessors *)
    1.27 +
    1.28 +fun trans_comb eq1 eq2 =
    1.29 +  if Thm.is_reflexive eq1 then eq2
    1.30 +  else if Thm.is_reflexive eq2 then eq1
    1.31 +  else Thm.transitive eq1 eq2;
    1.32 +
    1.33 +fun trans_conv_rule conv eq = trans_comb eq (conv (Thm.rhs_of eq));
    1.34 +
    1.35 +type sandwich = Proof.context -> cterm -> (thm -> thm) * cterm;
    1.36 +type conv_sandwich = Proof.context -> cterm -> conv * thm;
    1.37 +
    1.38 +fun chain sandwich2 sandwich1 ctxt =
    1.39 +  sandwich1 ctxt
    1.40 +  ##>> sandwich2 ctxt
    1.41 +  #>> (op o);
    1.42 +
    1.43 +fun lift_conv_sandwich conv_sandwhich ctxt ct =
    1.44 +  let
    1.45 +    val (postproc_conv, eq) = conv_sandwhich ctxt ct;
    1.46 +  in (trans_conv_rule postproc_conv o trans_comb eq, Thm.rhs_of eq) end;
    1.47 +
    1.48 +fun finalize 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 +
    1.53 +fun evaluation sandwich lift_postproc eval ctxt t =
    1.54 +  let
    1.55 +    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    1.56 +    val (postproc, ct') = sandwich ctxt (cert t);
    1.57 +  in
    1.58 +    term_of ct'
    1.59 +    |> eval ctxt
    1.60 +    |> lift_postproc (term_of o Thm.rhs_of o postproc o Thm.reflexive o cert)
    1.61 +  end;
    1.62 +
    1.63 +
    1.64  (* post- and preprocessing *)
    1.65  
    1.66 -fun no_variables_conv ctxt conv ct =
    1.67 -  let
    1.68 -    val thy = Proof_Context.theory_of ctxt;
    1.69 -    val cert = Thm.cterm_of thy;
    1.70 -    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
    1.71 -      | t as Var _ => insert (op aconvc) (cert t)
    1.72 -      | _ => I) (Thm.term_of ct) [];
    1.73 -    fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
    1.74 -      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
    1.75 -      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
    1.76 -  in
    1.77 -    ct
    1.78 -    |> fold_rev Thm.lambda all_vars
    1.79 -    |> conv
    1.80 -    |> fold apply_beta all_vars
    1.81 -  end;
    1.82 -
    1.83 -fun normalized_tfrees ctxt conv ct =
    1.84 +fun normalized_tfrees_sandwich ctxt ct =
    1.85    let
    1.86      val cert = cterm_of (Proof_Context.theory_of ctxt);
    1.87      val t = term_of ct;
    1.88 @@ -136,58 +157,41 @@
    1.89      val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
    1.90      val normalization =
    1.91        map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized;
    1.92 -    val ct_normalized = cert (map_types normalize t);
    1.93    in
    1.94 -    ct_normalized
    1.95 -    |> conv
    1.96 -    |> Thm.varifyT_global
    1.97 -    |> Thm.certify_instantiate (normalization, [])
    1.98 +    (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
    1.99    end;
   1.100  
   1.101 -fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   1.102 -
   1.103 -fun term_of_conv ctxt conv =
   1.104 -  Thm.cterm_of (Proof_Context.theory_of ctxt)
   1.105 -  #> conv ctxt
   1.106 -  #> Thm.prop_of
   1.107 -  #> Logic.dest_equals
   1.108 -  #> snd;
   1.109 +fun no_variables_sandwich ctxt ct =
   1.110 +  let
   1.111 +    val thy = Proof_Context.theory_of ctxt;
   1.112 +    val cert = Thm.cterm_of thy;
   1.113 +    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
   1.114 +      | t as Var _ => insert (op aconvc) (cert t)
   1.115 +      | _ => I) (Thm.term_of ct) [];
   1.116 +    fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
   1.117 +      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
   1.118 +      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
   1.119 +  in (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct) end;
   1.120  
   1.121 -fun term_of_conv_resubst ctxt conv t =
   1.122 -  let
   1.123 -    val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
   1.124 -      | t as Var _ => insert (op aconv) t
   1.125 -      | _ => I) t [];
   1.126 -    val resubst = curry (Term.betapplys o swap) all_vars;
   1.127 -  in (resubst, term_of_conv ctxt conv (fold_rev lambda all_vars t)) end;
   1.128 -
   1.129 -fun preprocess_conv ctxt =
   1.130 +fun simplifier_conv_sandwich ctxt =
   1.131    let
   1.132      val thy = Proof_Context.theory_of ctxt;
   1.133 -    val ss = (#pre o the_thmproc) thy;
   1.134 -  in fn ctxt' =>
   1.135 -    Simplifier.rewrite (put_simpset ss ctxt')
   1.136 -    #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
   1.137 -  end;
   1.138 -
   1.139 -fun preprocess_term ctxt =
   1.140 -  let
   1.141 -    val conv = preprocess_conv ctxt;
   1.142 -  in fn ctxt' => term_of_conv_resubst ctxt' conv end;
   1.143 +    val pre = (#pre o the_thmproc) thy;
   1.144 +    val post = (#post o the_thmproc) thy;
   1.145 +    fun pre_conv ctxt' =
   1.146 +      Simplifier.rewrite (put_simpset pre ctxt')
   1.147 +      #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
   1.148 +    fun post_conv ctxt' =
   1.149 +      Axclass.overload_conv (Proof_Context.theory_of ctxt')
   1.150 +      #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'))
   1.151 +  in fn ctxt' => pre_conv ctxt' #> pair (post_conv ctxt') end;
   1.152  
   1.153 -fun postprocess_conv ctxt =
   1.154 -  let
   1.155 -    val thy = Proof_Context.theory_of ctxt;
   1.156 -    val ss = (#post o the_thmproc) thy;
   1.157 -  in fn ctxt' =>
   1.158 -    Axclass.overload_conv (Proof_Context.theory_of ctxt')
   1.159 -    #> trans_conv_rule (Simplifier.rewrite (put_simpset ss ctxt'))
   1.160 -  end;
   1.161 +fun simplifier_sandwich ctxt = lift_conv_sandwich (simplifier_conv_sandwich ctxt);
   1.162  
   1.163 -fun postprocess_term ctxt =
   1.164 -  let
   1.165 -    val conv = postprocess_conv ctxt;
   1.166 -  in fn ctxt' => term_of_conv ctxt' conv end;
   1.167 +fun value_sandwich ctxt =
   1.168 +  normalized_tfrees_sandwich
   1.169 +  |> chain no_variables_sandwich
   1.170 +  |> chain (simplifier_sandwich ctxt);
   1.171  
   1.172  fun print_codeproc ctxt =
   1.173    let
   1.174 @@ -477,57 +481,28 @@
   1.175    (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
   1.176      (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
   1.177  
   1.178 -fun dynamic_conv ctxt conv = normalized_tfrees ctxt (no_variables_conv ctxt (fn ct =>
   1.179 +fun dynamic_evaluator eval ctxt t =
   1.180    let
   1.181 -    val thm1 = preprocess_conv ctxt ctxt ct;
   1.182 -    val ct' = Thm.rhs_of thm1;
   1.183 -    val t' = Thm.term_of ct';
   1.184      val consts = fold_aterms
   1.185 -      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
   1.186 -    val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
   1.187 -    val thm2 = conv algebra' eqngr' t' ct';
   1.188 -    val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2);
   1.189 -  in
   1.190 -    Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   1.191 -      error ("could not construct evaluation proof:\n"
   1.192 -      ^ (cat_lines o map (Display.string_of_thm ctxt)) [thm1, thm2, thm3])
   1.193 -  end));
   1.194 +      (fn Const (c, _) => insert (op =) c | _ => I) t [];
   1.195 +    val (algebra, eqngr) = obtain false (Proof_Context.theory_of ctxt) consts [t];
   1.196 +  in eval algebra eqngr t end;
   1.197  
   1.198 -fun dynamic_value ctxt postproc evaluator t =
   1.199 -  let
   1.200 -    val (resubst, t') = preprocess_term ctxt ctxt t;
   1.201 -    val consts = fold_aterms
   1.202 -      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
   1.203 -    val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
   1.204 -  in
   1.205 -    t'
   1.206 -    |> evaluator algebra' eqngr'
   1.207 -    |> postproc (postprocess_term ctxt ctxt o resubst)
   1.208 -  end;
   1.209 +fun dynamic_conv ctxt conv =
   1.210 +  finalize (value_sandwich ctxt) (dynamic_evaluator conv) ctxt;
   1.211 +
   1.212 +fun dynamic_value ctxt lift_postproc evaluator =
   1.213 +  evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
   1.214  
   1.215  fun static_conv ctxt consts conv =
   1.216    let
   1.217      val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
   1.218 -    val pre_conv = preprocess_conv ctxt;
   1.219 -    val conv' = conv algebra eqngr;
   1.220 -    val post_conv = postprocess_conv ctxt;
   1.221 -  in fn ctxt' => normalized_tfrees ctxt' (no_variables_conv ctxt' ((pre_conv ctxt')
   1.222 -    then_conv (fn ct => conv' ctxt' (Thm.term_of ct) ct)
   1.223 -    then_conv (post_conv ctxt')))
   1.224 -  end;
   1.225 +  in finalize (value_sandwich ctxt) (conv algebra eqngr) end;
   1.226  
   1.227 -fun static_value ctxt postproc consts evaluator =
   1.228 +fun static_value ctxt lift_postproc consts evaluator =
   1.229    let
   1.230      val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
   1.231 -    val preproc = preprocess_term ctxt;
   1.232 -    val evaluator' = evaluator algebra eqngr;
   1.233 -    val postproc' = postprocess_term ctxt;
   1.234 -  in fn ctxt' => 
   1.235 -    preproc ctxt'
   1.236 -    #-> (fn resubst => fn t => t
   1.237 -      |> evaluator' ctxt'
   1.238 -      |> postproc (postproc' ctxt' o resubst))
   1.239 -  end;
   1.240 +  in evaluation (value_sandwich ctxt) lift_postproc (evaluator algebra eqngr) end;
   1.241  
   1.242  
   1.243  (** setup **)