author haftmann Mon Feb 06 20:56:33 2017 +0100 (2017-02-06) changeset 64989 40c36a4aee1f parent 64988 93aaff2b0ae0 child 64990 c6a7de505796
more computation antiquotations
 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	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 =
```