src/Tools/Code/code_runtime.ML
changeset 64993 4fb84597ec5a
parent 64992 41e2c3617582
child 64995 a7af4045f873
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:36 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:37 2017 +0100
     1.3 @@ -361,6 +361,48 @@
     1.4          ] |> rpair of_term_names
     1.5        end;
     1.6  
     1.7 +
     1.8 +(* dedicated preprocessor for computations *)
     1.9 +
    1.10 +structure Computation_Preproc_Data = Theory_Data
    1.11 +(
    1.12 +  type T = thm list;
    1.13 +  val empty = [];
    1.14 +  val extend = I;
    1.15 +  val merge = Library.merge Thm.eq_thm_prop;
    1.16 +);
    1.17 +
    1.18 +local
    1.19 +
    1.20 +fun add thm thy =
    1.21 +  let
    1.22 +    val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm;
    1.23 +  in
    1.24 +    thy
    1.25 +    |> Computation_Preproc_Data.map (union Thm.eq_thm_prop thms)
    1.26 +  end;
    1.27 +
    1.28 +fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt);
    1.29 +
    1.30 +in
    1.31 +
    1.32 +fun preprocess_conv ctxt = 
    1.33 +  Raw_Simplifier.rewrite ctxt false (get ctxt);
    1.34 +
    1.35 +fun preprocess_term ctxt =
    1.36 +  Pattern.rewrite_term (Proof_Context.theory_of ctxt)
    1.37 +    (map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt)) [];
    1.38 +
    1.39 +val _ = Theory.setup
    1.40 +  (Attrib.setup @{binding code_computation_unfold}
    1.41 +    (Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add thm) I)))
    1.42 +    "preprocessing equations for computation");
    1.43 +
    1.44 +end;
    1.45 +
    1.46 +
    1.47 +(* mounting computations *)
    1.48 +
    1.49  fun prechecked_computation T raw_computation ctxt =
    1.50    check_typ ctxt T
    1.51    #> reject_vars ctxt
    1.52 @@ -376,17 +418,21 @@
    1.53    #> partiality_as_none;
    1.54  
    1.55  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    1.56 -  prechecked_computation T (Code_Preproc.static_value
    1.57 -    { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.58 -    (K (checked_computation cTs raw_computation)));
    1.59 +  let
    1.60 +    val computation = prechecked_computation T (Code_Preproc.static_value
    1.61 +      { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.62 +      (K (checked_computation cTs raw_computation)));
    1.63 +  in fn ctxt' => preprocess_term ctxt' #> computation ctxt' end;
    1.64  
    1.65  fun mount_computation_conv ctxt cTs T raw_computation conv =
    1.66 -  prechecked_conv T (Code_Preproc.static_conv
    1.67 -    { ctxt = ctxt, consts = [] }
    1.68 -    (K (fn ctxt' => fn t =>
    1.69 -      case checked_computation cTs raw_computation ctxt' t of
    1.70 -        SOME x => conv x
    1.71 -      | NONE => Conv.all_conv)));
    1.72 +  let
    1.73 +    val computation_conv = prechecked_conv T (Code_Preproc.static_conv
    1.74 +      { ctxt = ctxt, consts = [] }
    1.75 +      (K (fn ctxt' => fn t =>
    1.76 +        case checked_computation cTs raw_computation ctxt' t of
    1.77 +          SOME x => conv x
    1.78 +        | NONE => Conv.all_conv)));
    1.79 +  in fn ctxt' => preprocess_conv ctxt' then_conv computation_conv ctxt' end;
    1.80  
    1.81  local
    1.82  
    1.83 @@ -517,7 +563,8 @@
    1.84      fun generated_code' () =
    1.85        let
    1.86          val evals = Abs ("eval", map snd computation_cTs' --->
    1.87 -          TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs'));
    1.88 +          TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs'))
    1.89 +          |> preprocess_term ctxt
    1.90        in Code_Thingol.dynamic_value ctxt
    1.91          (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals
    1.92        end;
    1.93 @@ -727,24 +774,15 @@
    1.94  
    1.95  in
    1.96  
    1.97 -val _ =
    1.98 -  Theory.setup (ML_Antiquotation.declaration @{binding code}
    1.99 -    Args.term (fn _ => ml_code_antiq));
   1.100 -
   1.101 -val _ =
   1.102 -  Theory.setup (ML_Antiquotation.declaration @{binding computation}
   1.103 -    (Args.typ -- parse_consts_spec)
   1.104 -       (fn _ => ml_computation_antiq));
   1.105 -
   1.106 -val _ =
   1.107 -  Theory.setup (ML_Antiquotation.declaration @{binding computation_conv}
   1.108 -    (Args.typ -- parse_consts_spec)
   1.109 -       (fn _ => ml_computation_conv_antiq));
   1.110 -
   1.111 -val _ =
   1.112 -  Theory.setup (ML_Antiquotation.declaration @{binding computation_check}
   1.113 -    parse_consts_spec 
   1.114 -       (fn _ => ml_computation_check_antiq));
   1.115 +val _ = Theory.setup
   1.116 +  (ML_Antiquotation.declaration @{binding code}
   1.117 +    Args.term (K ml_code_antiq)
   1.118 +  #> ML_Antiquotation.declaration @{binding computation}
   1.119 +    (Args.typ -- parse_consts_spec) (K ml_computation_antiq)
   1.120 +  #> ML_Antiquotation.declaration @{binding computation_conv}
   1.121 +    (Args.typ -- parse_consts_spec) (K ml_computation_conv_antiq)
   1.122 +  #> ML_Antiquotation.declaration @{binding computation_check}
   1.123 +    parse_consts_spec (K ml_computation_check_antiq));
   1.124  
   1.125  end;
   1.126