src/Tools/Code/code_runtime.ML
changeset 64989 40c36a4aee1f
parent 64988 93aaff2b0ae0
child 64990 c6a7de505796
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:32 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:33 2017 +0100
     1.3 @@ -34,6 +34,10 @@
     1.4    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
     1.5    val mount_computation: Proof.context -> (string * typ) list -> typ
     1.6      -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     1.7 +  val mount_computation_conv: Proof.context -> (string * typ) list -> typ
     1.8 +    -> (term -> 'ml) -> ('ml -> conv) -> Proof.context -> conv
     1.9 +  val mount_computation_check: Proof.context -> (string * typ) list
    1.10 +    -> (term -> truth) -> Proof.context -> conv
    1.11    val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    1.12    val trace: bool Config.T
    1.13  end;
    1.14 @@ -361,6 +365,29 @@
    1.15    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    1.16      (K (checked_computation cTs T raw_computation));
    1.17  
    1.18 +fun mount_computation_conv ctxt cTs T raw_computation conv =
    1.19 +  Code_Preproc.static_conv { ctxt = ctxt, consts = [] }
    1.20 +    (K (fn ctxt' => fn t =>
    1.21 +      case checked_computation cTs T raw_computation ctxt' t of
    1.22 +        SOME x => conv x
    1.23 +      | NONE => Conv.all_conv));
    1.24 +
    1.25 +local
    1.26 +
    1.27 +fun holds ct = Thm.mk_binop @{cterm "Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop"}
    1.28 +  ct @{cprop "PROP Code_Generator.holds"};
    1.29 +
    1.30 +val (_, holds_oracle) = Context.>>> (Context.map_theory_result
    1.31 +  (Thm.add_oracle (@{binding holds}, holds)));
    1.32 +
    1.33 +in
    1.34 +
    1.35 +fun mount_computation_check ctxt cTs raw_computation =
    1.36 +  mount_computation_conv ctxt cTs @{typ prop} raw_computation
    1.37 +    (K holds_oracle);
    1.38 +
    1.39 +end;
    1.40 +
    1.41  
    1.42  (** variants of universal runtime code generation **)
    1.43  
    1.44 @@ -437,9 +464,11 @@
    1.45  
    1.46  (** code and computation antiquotations **)
    1.47  
    1.48 -val mount_computationN = prefix_this "mount_computation";
    1.49 +local
    1.50  
    1.51 -local
    1.52 +val mount_computationN = prefix_this "mount_computation";
    1.53 +val mount_computation_convN = prefix_this "mount_computation_conv";
    1.54 +val mount_computation_checkN = prefix_this "mount_computation_check";
    1.55  
    1.56  structure Code_Antiq_Data = Proof_Data
    1.57  (
    1.58 @@ -502,23 +531,42 @@
    1.59      val position_index = current_position_index ctxt;
    1.60      val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt';
    1.61      val context_code = if position_index = 0 then code else "";
    1.62 -    val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt') position_index;
    1.63 +    val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt');
    1.64    in (context_code, body_code) end;
    1.65  
    1.66  fun print_code ctxt const =
    1.67 -  print (fn { name_for_const, ... } => fn prfx => fn _ =>
    1.68 +  print (fn { name_for_const, ... } => fn prfx =>
    1.69      Long_Name.append prfx (name_for_const const)) ctxt;
    1.70  
    1.71 -fun print_computation ctxt T =
    1.72 -  print (fn { of_term_for_typ, ... } => fn prfx => fn _ =>
    1.73 +fun print_computation kind ctxt T =
    1.74 +  print (fn { of_term_for_typ, ... } => fn prfx =>
    1.75      space_implode " " [
    1.76 -      mount_computationN,
    1.77 +      kind,
    1.78        "(Context.proof_of (Context.the_generic_context ()))",
    1.79        Long_Name.implode [prfx, generated_computationN, covered_constsN],
    1.80        (ML_Syntax.atomic o ML_Syntax.print_typ) T,
    1.81        Long_Name.append prfx (of_term_for_typ T)
    1.82      ]) ctxt;
    1.83  
    1.84 +fun print_computation_check ctxt =
    1.85 +  print (fn { of_term_for_typ, ... } => fn prfx =>
    1.86 +    space_implode " " [
    1.87 +      mount_computation_checkN,
    1.88 +      "(Context.proof_of (Context.the_generic_context ()))",
    1.89 +      Long_Name.implode [prfx, generated_computationN, covered_constsN],
    1.90 +      Long_Name.append prfx (of_term_for_typ @{typ prop})
    1.91 +    ]) ctxt;
    1.92 +
    1.93 +fun prep_terms ctxt raw_ts =
    1.94 +  let
    1.95 +    val ts = map (Syntax.check_term ctxt) raw_ts;
    1.96 +  in
    1.97 +    (fold o fold_aterms)
    1.98 +      (fn (t as Const (cT as (_, T))) =>
    1.99 +        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
   1.100 +        else insert (op =) cT | _ => I) ts []
   1.101 +  end;
   1.102 +
   1.103  in
   1.104  
   1.105  fun ml_code_antiq raw_const ctxt =
   1.106 @@ -527,18 +575,23 @@
   1.107      val const = Code.check_const thy raw_const;
   1.108    in (print_code ctxt const, register_const const ctxt) end;
   1.109  
   1.110 -fun ml_computation_antiq (raw_ts, raw_T) ctxt =
   1.111 +fun gen_ml_computation_antiq kind (raw_ts, raw_T) ctxt =
   1.112    let
   1.113 -    val ts = map (Syntax.check_term ctxt) raw_ts;
   1.114 -    val cTs = (fold o fold_aterms)
   1.115 -      (fn (t as Const (cT as (_, T))) =>
   1.116 -        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
   1.117 -        else insert (op =) cT | _ => I) ts [];
   1.118 +    val cTs = prep_terms ctxt raw_ts;
   1.119      val T = Syntax.check_typ ctxt raw_T;
   1.120      val _ = if not (monomorphic T)
   1.121        then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
   1.122        else ();
   1.123 -  in (print_computation ctxt T, register_computation cTs T ctxt) end;
   1.124 +  in (print_computation kind ctxt T, register_computation cTs T ctxt) end;
   1.125 +
   1.126 +val ml_computation_antiq = gen_ml_computation_antiq mount_computationN;
   1.127 +
   1.128 +val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN;
   1.129 +
   1.130 +fun ml_computation_check_antiq raw_ts ctxt =
   1.131 +  let
   1.132 +    val cTs = insert (op =) (dest_Const @{const holds}) (prep_terms ctxt raw_ts);
   1.133 +  in (print_computation_check ctxt, register_computation cTs @{typ prop} ctxt) end;
   1.134  
   1.135  end; (*local*)
   1.136  
   1.137 @@ -641,6 +694,16 @@
   1.138      (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
   1.139         (fn _ => ml_computation_antiq));
   1.140  
   1.141 +val _ =
   1.142 +  Theory.setup (ML_Antiquotation.declaration @{binding computation_conv}
   1.143 +    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
   1.144 +       (fn _ => ml_computation_conv_antiq));
   1.145 +
   1.146 +val _ =
   1.147 +  Theory.setup (ML_Antiquotation.declaration @{binding computation_check}
   1.148 +    (Scan.repeat Args.term) 
   1.149 +       (fn _ => ml_computation_check_antiq));
   1.150 +
   1.151  local
   1.152  
   1.153  val parse_datatype =