tuned
authorhaftmann
Mon Feb 06 20:56:30 2017 +0100 (2017-02-06)
changeset 649871985502518ce
parent 64986 b81a048960a3
child 64988 93aaff2b0ae0
tuned
src/HOL/ex/Computations.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/ex/Computations.thy	Sat Feb 04 21:15:11 2017 +0100
     1.2 +++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:30 2017 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  section \<open>Simple example for computations generated by the code generator\<close>
     1.5  
     1.6  theory Computations
     1.7 -  imports Nat Fun_Def Num Code_Numeral
     1.8 +  imports "../Nat" "../Fun_Def" "../Num" "../Code_Numeral"
     1.9  begin
    1.10  
    1.11  fun even :: "nat \<Rightarrow> bool"
    1.12 @@ -37,7 +37,7 @@
    1.13  
    1.14  val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
    1.15    HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
    1.16 -  (K I)
    1.17 +  (K I);
    1.18  
    1.19  end
    1.20  \<close>
     2.1 --- a/src/Tools/Code/code_runtime.ML	Sat Feb 04 21:15:11 2017 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:30 2017 +0100
     2.3 @@ -28,14 +28,14 @@
     2.4      -> Proof.context -> term -> 'a Exn.result
     2.5    val dynamic_holds_conv: Proof.context -> conv
     2.6    val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
     2.7 -  val mount_computation: Proof.context -> (string * typ) list -> typ
     2.8 -    -> (term -> 'b) -> ((term -> term) -> 'b -> 'a) -> Proof.context -> term -> 'a
     2.9    val code_reflect: (string * string list option) list -> string list -> string
    2.10      -> string option -> theory -> theory
    2.11    datatype truth = Holds
    2.12    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
    2.13 +  val mount_computation: Proof.context -> (string * typ) list -> typ
    2.14 +    -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
    2.15 +  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    2.16    val trace: bool Config.T
    2.17 -  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    2.18  end;
    2.19  
    2.20  structure Code_Runtime : CODE_RUNTIME =
    2.21 @@ -48,8 +48,9 @@
    2.22  (* technical prerequisites *)
    2.23  
    2.24  val thisN = "Code_Runtime";
    2.25 -val truthN = Long_Name.append thisN "truth";
    2.26 -val HoldsN = Long_Name.append thisN "Holds";
    2.27 +val prefix_this = Long_Name.append thisN;
    2.28 +val truthN = prefix_this "truth";
    2.29 +val HoldsN = prefix_this "Holds";
    2.30  
    2.31  val target = "Eval";
    2.32  
    2.33 @@ -151,7 +152,7 @@
    2.34    fun init _ = empty;
    2.35  );
    2.36  val put_truth = Truth_Result.put;
    2.37 -val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append thisN "put_truth");
    2.38 +val truth_cookie = (Truth_Result.get, put_truth, prefix_this "put_truth");
    2.39  
    2.40  local
    2.41  
    2.42 @@ -349,13 +350,15 @@
    2.43          ] |> rpair of_term_names
    2.44        end;
    2.45  
    2.46 +fun checked_computation cTs T raw_computation ctxt =
    2.47 +  check_typ ctxt T
    2.48 +  #> reject_vars ctxt
    2.49 +  #> check_computation_input ctxt cTs
    2.50 +  #> raw_computation;
    2.51 +
    2.52  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    2.53    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    2.54 -    (fn _ => fn ctxt' =>
    2.55 -      check_typ ctxt' T
    2.56 -      #> reject_vars ctxt'
    2.57 -      #> check_computation_input ctxt' cTs
    2.58 -      #> raw_computation);
    2.59 +    (K (checked_computation cTs T raw_computation));
    2.60  
    2.61  
    2.62  (** variants of universal runtime code generation **)
    2.63 @@ -433,7 +436,7 @@
    2.64  
    2.65  (** code and computation antiquotations **)
    2.66  
    2.67 -val mount_computationN = Long_Name.append thisN "mount_computation";
    2.68 +val mount_computationN = prefix_this "mount_computation";
    2.69  
    2.70  local
    2.71  
    2.72 @@ -526,14 +529,14 @@
    2.73  fun ml_computation_antiq (raw_ts, raw_T) ctxt =
    2.74    let
    2.75      val ts = map (Syntax.check_term ctxt) raw_ts;
    2.76 +    val cTs = (fold o fold_aterms)
    2.77 +      (fn (t as Const (cT as (_, T))) =>
    2.78 +        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
    2.79 +        else insert (op =) cT | _ => I) ts [];
    2.80      val T = Syntax.check_typ ctxt raw_T;
    2.81      val _ = if not (monomorphic T)
    2.82        then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
    2.83        else ();
    2.84 -    val cTs = (fold o fold_aterms)
    2.85 -      (fn (t as Const (cT as (_, T))) =>
    2.86 -        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
    2.87 -        else insert (op =) cT | _ => I) ts [];
    2.88    in (print_computation ctxt T, register_computation cTs T ctxt) end;
    2.89  
    2.90  end; (*local*)
    2.91 @@ -634,7 +637,8 @@
    2.92  
    2.93  val _ =
    2.94    Theory.setup (ML_Antiquotation.declaration @{binding computation}
    2.95 -    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ) (fn _ => ml_computation_antiq));
    2.96 +    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
    2.97 +       (fn _ => ml_computation_antiq));
    2.98  
    2.99  local
   2.100