src/Tools/Code/code_runtime.ML
changeset 64987 1985502518ce
parent 64959 9ca021bd718d
child 64988 93aaff2b0ae0
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Feb 04 21:15:11 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:30 2017 +0100
     1.3 @@ -28,14 +28,14 @@
     1.4      -> Proof.context -> term -> 'a Exn.result
     1.5    val dynamic_holds_conv: Proof.context -> conv
     1.6    val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
     1.7 -  val mount_computation: Proof.context -> (string * typ) list -> typ
     1.8 -    -> (term -> 'b) -> ((term -> term) -> 'b -> 'a) -> Proof.context -> term -> 'a
     1.9    val code_reflect: (string * string list option) list -> string list -> string
    1.10      -> string option -> theory -> theory
    1.11    datatype truth = Holds
    1.12    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
    1.13 +  val mount_computation: Proof.context -> (string * typ) list -> typ
    1.14 +    -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
    1.15 +  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    1.16    val trace: bool Config.T
    1.17 -  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    1.18  end;
    1.19  
    1.20  structure Code_Runtime : CODE_RUNTIME =
    1.21 @@ -48,8 +48,9 @@
    1.22  (* technical prerequisites *)
    1.23  
    1.24  val thisN = "Code_Runtime";
    1.25 -val truthN = Long_Name.append thisN "truth";
    1.26 -val HoldsN = Long_Name.append thisN "Holds";
    1.27 +val prefix_this = Long_Name.append thisN;
    1.28 +val truthN = prefix_this "truth";
    1.29 +val HoldsN = prefix_this "Holds";
    1.30  
    1.31  val target = "Eval";
    1.32  
    1.33 @@ -151,7 +152,7 @@
    1.34    fun init _ = empty;
    1.35  );
    1.36  val put_truth = Truth_Result.put;
    1.37 -val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append thisN "put_truth");
    1.38 +val truth_cookie = (Truth_Result.get, put_truth, prefix_this "put_truth");
    1.39  
    1.40  local
    1.41  
    1.42 @@ -349,13 +350,15 @@
    1.43          ] |> rpair of_term_names
    1.44        end;
    1.45  
    1.46 +fun checked_computation cTs T raw_computation ctxt =
    1.47 +  check_typ ctxt T
    1.48 +  #> reject_vars ctxt
    1.49 +  #> check_computation_input ctxt cTs
    1.50 +  #> raw_computation;
    1.51 +
    1.52  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    1.53    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.54 -    (fn _ => fn ctxt' =>
    1.55 -      check_typ ctxt' T
    1.56 -      #> reject_vars ctxt'
    1.57 -      #> check_computation_input ctxt' cTs
    1.58 -      #> raw_computation);
    1.59 +    (K (checked_computation cTs T raw_computation));
    1.60  
    1.61  
    1.62  (** variants of universal runtime code generation **)
    1.63 @@ -433,7 +436,7 @@
    1.64  
    1.65  (** code and computation antiquotations **)
    1.66  
    1.67 -val mount_computationN = Long_Name.append thisN "mount_computation";
    1.68 +val mount_computationN = prefix_this "mount_computation";
    1.69  
    1.70  local
    1.71  
    1.72 @@ -526,14 +529,14 @@
    1.73  fun ml_computation_antiq (raw_ts, raw_T) ctxt =
    1.74    let
    1.75      val ts = map (Syntax.check_term ctxt) raw_ts;
    1.76 +    val cTs = (fold o fold_aterms)
    1.77 +      (fn (t as Const (cT as (_, T))) =>
    1.78 +        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
    1.79 +        else insert (op =) cT | _ => I) ts [];
    1.80      val T = Syntax.check_typ ctxt raw_T;
    1.81      val _ = if not (monomorphic T)
    1.82        then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
    1.83        else ();
    1.84 -    val cTs = (fold o fold_aterms)
    1.85 -      (fn (t as Const (cT as (_, T))) =>
    1.86 -        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
    1.87 -        else insert (op =) cT | _ => I) ts [];
    1.88    in (print_computation ctxt T, register_computation cTs T ctxt) end;
    1.89  
    1.90  end; (*local*)
    1.91 @@ -634,7 +637,8 @@
    1.92  
    1.93  val _ =
    1.94    Theory.setup (ML_Antiquotation.declaration @{binding computation}
    1.95 -    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ) (fn _ => ml_computation_antiq));
    1.96 +    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
    1.97 +       (fn _ => ml_computation_antiq));
    1.98  
    1.99  local
   1.100