more computation antiquotations
authorhaftmann
Mon Feb 06 20:56:33 2017 +0100 (2017-02-06)
changeset 6498940c36a4aee1f
parent 64988 93aaff2b0ae0
child 64990 c6a7de505796
more computation antiquotations
src/HOL/ex/Computations.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:32 2017 +0100
     1.2 +++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:33 2017 +0100
     1.3 @@ -36,9 +36,11 @@
     1.4    (fn post => post o HOLogic.mk_nat o int_of_nat o the);
     1.5  
     1.6  val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
     1.7 -  HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
     1.8 +  HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool}
     1.9    (K the);
    1.10  
    1.11 +val comp_check = @{computation_check Trueprop};
    1.12 +
    1.13  end
    1.14  \<close>
    1.15  
    1.16 @@ -55,6 +57,10 @@
    1.17  \<close>
    1.18  
    1.19  ML_val \<open>
    1.20 +  comp_check @{context} @{cprop "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))"}
    1.21 +\<close>
    1.22 +  
    1.23 +ML_val \<open>
    1.24    comp_numeral @{context} @{term "Suc 42 + 7"}
    1.25    |> Syntax.string_of_term @{context}
    1.26    |> writeln
     2.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:32 2017 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:33 2017 +0100
     2.3 @@ -34,6 +34,10 @@
     2.4    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
     2.5    val mount_computation: Proof.context -> (string * typ) list -> typ
     2.6      -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     2.7 +  val mount_computation_conv: Proof.context -> (string * typ) list -> typ
     2.8 +    -> (term -> 'ml) -> ('ml -> conv) -> Proof.context -> conv
     2.9 +  val mount_computation_check: Proof.context -> (string * typ) list
    2.10 +    -> (term -> truth) -> Proof.context -> conv
    2.11    val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    2.12    val trace: bool Config.T
    2.13  end;
    2.14 @@ -361,6 +365,29 @@
    2.15    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
    2.16      (K (checked_computation cTs T raw_computation));
    2.17  
    2.18 +fun mount_computation_conv ctxt cTs T raw_computation conv =
    2.19 +  Code_Preproc.static_conv { ctxt = ctxt, consts = [] }
    2.20 +    (K (fn ctxt' => fn t =>
    2.21 +      case checked_computation cTs T raw_computation ctxt' t of
    2.22 +        SOME x => conv x
    2.23 +      | NONE => Conv.all_conv));
    2.24 +
    2.25 +local
    2.26 +
    2.27 +fun holds ct = Thm.mk_binop @{cterm "Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop"}
    2.28 +  ct @{cprop "PROP Code_Generator.holds"};
    2.29 +
    2.30 +val (_, holds_oracle) = Context.>>> (Context.map_theory_result
    2.31 +  (Thm.add_oracle (@{binding holds}, holds)));
    2.32 +
    2.33 +in
    2.34 +
    2.35 +fun mount_computation_check ctxt cTs raw_computation =
    2.36 +  mount_computation_conv ctxt cTs @{typ prop} raw_computation
    2.37 +    (K holds_oracle);
    2.38 +
    2.39 +end;
    2.40 +
    2.41  
    2.42  (** variants of universal runtime code generation **)
    2.43  
    2.44 @@ -437,9 +464,11 @@
    2.45  
    2.46  (** code and computation antiquotations **)
    2.47  
    2.48 -val mount_computationN = prefix_this "mount_computation";
    2.49 +local
    2.50  
    2.51 -local
    2.52 +val mount_computationN = prefix_this "mount_computation";
    2.53 +val mount_computation_convN = prefix_this "mount_computation_conv";
    2.54 +val mount_computation_checkN = prefix_this "mount_computation_check";
    2.55  
    2.56  structure Code_Antiq_Data = Proof_Data
    2.57  (
    2.58 @@ -502,23 +531,42 @@
    2.59      val position_index = current_position_index ctxt;
    2.60      val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt';
    2.61      val context_code = if position_index = 0 then code else "";
    2.62 -    val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt') position_index;
    2.63 +    val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt');
    2.64    in (context_code, body_code) end;
    2.65  
    2.66  fun print_code ctxt const =
    2.67 -  print (fn { name_for_const, ... } => fn prfx => fn _ =>
    2.68 +  print (fn { name_for_const, ... } => fn prfx =>
    2.69      Long_Name.append prfx (name_for_const const)) ctxt;
    2.70  
    2.71 -fun print_computation ctxt T =
    2.72 -  print (fn { of_term_for_typ, ... } => fn prfx => fn _ =>
    2.73 +fun print_computation kind ctxt T =
    2.74 +  print (fn { of_term_for_typ, ... } => fn prfx =>
    2.75      space_implode " " [
    2.76 -      mount_computationN,
    2.77 +      kind,
    2.78        "(Context.proof_of (Context.the_generic_context ()))",
    2.79        Long_Name.implode [prfx, generated_computationN, covered_constsN],
    2.80        (ML_Syntax.atomic o ML_Syntax.print_typ) T,
    2.81        Long_Name.append prfx (of_term_for_typ T)
    2.82      ]) ctxt;
    2.83  
    2.84 +fun print_computation_check ctxt =
    2.85 +  print (fn { of_term_for_typ, ... } => fn prfx =>
    2.86 +    space_implode " " [
    2.87 +      mount_computation_checkN,
    2.88 +      "(Context.proof_of (Context.the_generic_context ()))",
    2.89 +      Long_Name.implode [prfx, generated_computationN, covered_constsN],
    2.90 +      Long_Name.append prfx (of_term_for_typ @{typ prop})
    2.91 +    ]) ctxt;
    2.92 +
    2.93 +fun prep_terms ctxt raw_ts =
    2.94 +  let
    2.95 +    val ts = map (Syntax.check_term ctxt) raw_ts;
    2.96 +  in
    2.97 +    (fold o fold_aterms)
    2.98 +      (fn (t as Const (cT as (_, T))) =>
    2.99 +        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
   2.100 +        else insert (op =) cT | _ => I) ts []
   2.101 +  end;
   2.102 +
   2.103  in
   2.104  
   2.105  fun ml_code_antiq raw_const ctxt =
   2.106 @@ -527,18 +575,23 @@
   2.107      val const = Code.check_const thy raw_const;
   2.108    in (print_code ctxt const, register_const const ctxt) end;
   2.109  
   2.110 -fun ml_computation_antiq (raw_ts, raw_T) ctxt =
   2.111 +fun gen_ml_computation_antiq kind (raw_ts, raw_T) ctxt =
   2.112    let
   2.113 -    val ts = map (Syntax.check_term ctxt) raw_ts;
   2.114 -    val cTs = (fold o fold_aterms)
   2.115 -      (fn (t as Const (cT as (_, T))) =>
   2.116 -        if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
   2.117 -        else insert (op =) cT | _ => I) ts [];
   2.118 +    val cTs = prep_terms ctxt raw_ts;
   2.119      val T = Syntax.check_typ ctxt raw_T;
   2.120      val _ = if not (monomorphic T)
   2.121        then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
   2.122        else ();
   2.123 -  in (print_computation ctxt T, register_computation cTs T ctxt) end;
   2.124 +  in (print_computation kind ctxt T, register_computation cTs T ctxt) end;
   2.125 +
   2.126 +val ml_computation_antiq = gen_ml_computation_antiq mount_computationN;
   2.127 +
   2.128 +val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN;
   2.129 +
   2.130 +fun ml_computation_check_antiq raw_ts ctxt =
   2.131 +  let
   2.132 +    val cTs = insert (op =) (dest_Const @{const holds}) (prep_terms ctxt raw_ts);
   2.133 +  in (print_computation_check ctxt, register_computation cTs @{typ prop} ctxt) end;
   2.134  
   2.135  end; (*local*)
   2.136  
   2.137 @@ -641,6 +694,16 @@
   2.138      (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
   2.139         (fn _ => ml_computation_antiq));
   2.140  
   2.141 +val _ =
   2.142 +  Theory.setup (ML_Antiquotation.declaration @{binding computation_conv}
   2.143 +    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
   2.144 +       (fn _ => ml_computation_conv_antiq));
   2.145 +
   2.146 +val _ =
   2.147 +  Theory.setup (ML_Antiquotation.declaration @{binding computation_check}
   2.148 +    (Scan.repeat Args.term) 
   2.149 +       (fn _ => ml_computation_check_antiq));
   2.150 +
   2.151  local
   2.152  
   2.153  val parse_datatype =