extended syntax allows to include datatype constructors directly in computations
authorhaftmann
Mon Feb 06 20:56:36 2017 +0100 (2017-02-06)
changeset 6499241e2c3617582
parent 64991 d2c79b16e133
child 64993 4fb84597ec5a
extended syntax allows to include datatype constructors directly in computations
src/HOL/ex/Computations.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:35 2017 +0100
     1.2 +++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:36 2017 +0100
     1.3 @@ -28,18 +28,25 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val comp_nat = @{computation "0 :: nat" Suc
     1.8 -  "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib :: nat}
     1.9 +val comp_nat = @{computation nat
    1.10 +  terms: "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib
    1.11 +  datatypes: nat}
    1.12 +  (fn post => post o HOLogic.mk_nat o int_of_nat o the);
    1.13 +
    1.14 +val comp_numeral = @{computation nat
    1.15 +  terms: "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat"}
    1.16    (fn post => post o HOLogic.mk_nat o int_of_nat o the);
    1.17  
    1.18 -val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat}
    1.19 -  (fn post => post o HOLogic.mk_nat o int_of_nat o the);
    1.20 -
    1.21 -val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
    1.22 -  HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool}
    1.23 +val comp_bool = @{computation bool
    1.24 +  terms: HOL.conj HOL.disj HOL.implies
    1.25 +    HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _"
    1.26 +  datatypes: bool}
    1.27    (K the);
    1.28  
    1.29 -val comp_check = @{computation_check Trueprop};
    1.30 +val comp_check = @{computation_check terms: Trueprop};
    1.31 +
    1.32 +val comp_dummy = @{computation "(nat \<times> unit) option"
    1.33 +  datatypes: "(nat \<times> unit) option"}
    1.34  
    1.35  end
    1.36  \<close>
     2.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:35 2017 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:36 2017 +0100
     2.3 @@ -573,14 +573,32 @@
     2.4        Long_Name.append prfx (of_term_for_typ @{typ prop})
     2.5      ]) ctxt;
     2.6  
     2.7 -fun prep_terms ctxt raw_ts =
     2.8 +
     2.9 +fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
    2.10 +  let
    2.11 +    val ((vs, constrs), _) = Code.get_type (Proof_Context.theory_of ctxt) tyco;
    2.12 +    val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
    2.13 +    val cs = map (fn (c, (_, Ts')) =>
    2.14 +      (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
    2.15 +        ---> dT)) constrs;
    2.16 +  in
    2.17 +    union (op =) cs
    2.18 +    #> fold (add_all_constrs ctxt) Ts
    2.19 +  end;
    2.20 +
    2.21 +fun prep_spec ctxt (raw_ts, raw_dTs) =
    2.22    let
    2.23      val ts = map (Syntax.check_term ctxt) raw_ts;
    2.24 +    val dTs = map (Syntax.check_typ ctxt) raw_dTs;
    2.25    in
    2.26 -    (fold o fold_aterms)
    2.27 +    []
    2.28 +    |> (fold o fold_aterms)
    2.29        (fn (t as Const (cT as (_, T))) =>
    2.30          if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
    2.31 -        else insert (op =) cT | _ => I) ts []
    2.32 +        else insert (op =) cT | _ => I) ts
    2.33 +    |> fold (fn dT =>
    2.34 +        if not (monomorphic dT) then error ("Polymorphic datatype: " ^ Syntax.string_of_typ ctxt dT)
    2.35 +        else add_all_constrs ctxt dT) dTs
    2.36    end;
    2.37  
    2.38  in
    2.39 @@ -591,9 +609,9 @@
    2.40      val const = Code.check_const thy raw_const;
    2.41    in (print_code ctxt const, register_const const ctxt) end;
    2.42  
    2.43 -fun gen_ml_computation_antiq kind (raw_ts, raw_T) ctxt =
    2.44 +fun gen_ml_computation_antiq kind (raw_T, raw_spec) ctxt =
    2.45    let
    2.46 -    val cTs = prep_terms ctxt raw_ts;
    2.47 +    val cTs = prep_spec ctxt raw_spec;
    2.48      val T = Syntax.check_typ ctxt raw_T;
    2.49      val _ = if not (monomorphic T)
    2.50        then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
    2.51 @@ -604,9 +622,9 @@
    2.52  
    2.53  val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN;
    2.54  
    2.55 -fun ml_computation_check_antiq raw_ts ctxt =
    2.56 +fun ml_computation_check_antiq raw_spec ctxt =
    2.57    let
    2.58 -    val cTs = insert (op =) (dest_Const @{const holds}) (prep_terms ctxt raw_ts);
    2.59 +    val cTs = insert (op =) (dest_Const @{const holds}) (prep_spec ctxt raw_spec);
    2.60    in (print_computation_check ctxt, register_computation cTs @{typ prop} ctxt) end;
    2.61  
    2.62  end; (*local*)
    2.63 @@ -701,25 +719,35 @@
    2.64  
    2.65  (** Isar setup **)
    2.66  
    2.67 +local
    2.68 +
    2.69 +val parse_consts_spec =
    2.70 +  Scan.optional (Scan.lift (Args.$$$ "terms" -- Args.colon) |-- Scan.repeat1 Args.term) []
    2.71 +  -- Scan.optional (Scan.lift (Args.$$$ "datatypes"  -- Args.colon) |-- Scan.repeat1 Args.typ) [];
    2.72 +
    2.73 +in
    2.74 +
    2.75  val _ =
    2.76    Theory.setup (ML_Antiquotation.declaration @{binding code}
    2.77      Args.term (fn _ => ml_code_antiq));
    2.78  
    2.79  val _ =
    2.80    Theory.setup (ML_Antiquotation.declaration @{binding computation}
    2.81 -    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
    2.82 +    (Args.typ -- parse_consts_spec)
    2.83         (fn _ => ml_computation_antiq));
    2.84  
    2.85  val _ =
    2.86    Theory.setup (ML_Antiquotation.declaration @{binding computation_conv}
    2.87 -    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
    2.88 +    (Args.typ -- parse_consts_spec)
    2.89         (fn _ => ml_computation_conv_antiq));
    2.90  
    2.91  val _ =
    2.92    Theory.setup (ML_Antiquotation.declaration @{binding computation_check}
    2.93 -    (Scan.repeat Args.term) 
    2.94 +    parse_consts_spec 
    2.95         (fn _ => ml_computation_check_antiq));
    2.96  
    2.97 +end;
    2.98 +
    2.99  local
   2.100  
   2.101  val parse_datatype =