author haftmann Mon Feb 06 20:56:30 2017 +0100 (2017-02-06) changeset 64987 1985502518ce parent 64986 b81a048960a3 child 64988 93aaff2b0ae0
tuned
 src/HOL/ex/Computations.thy file | annotate | diff | revisions src/Tools/Code/code_runtime.ML file | annotate | diff | revisions
```     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
```