src/Tools/Code/code_runtime.ML
changeset 64992 41e2c3617582
parent 64991 d2c79b16e133
child 64993 4fb84597ec5a
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:35 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:36 2017 +0100
     1.3 @@ -573,14 +573,32 @@
     1.4        Long_Name.append prfx (of_term_for_typ @{typ prop})
     1.5      ]) ctxt;
     1.6  
     1.7 -fun prep_terms ctxt raw_ts =
     1.8 +
     1.9 +fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
    1.10 +  let
    1.11 +    val ((vs, constrs), _) = Code.get_type (Proof_Context.theory_of ctxt) tyco;
    1.12 +    val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
    1.13 +    val cs = map (fn (c, (_, Ts')) =>
    1.14 +      (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
    1.15 +        ---> dT)) constrs;
    1.16 +  in
    1.17 +    union (op =) cs
    1.18 +    #> fold (add_all_constrs ctxt) Ts
    1.19 +  end;
    1.20 +
    1.21 +fun prep_spec ctxt (raw_ts, raw_dTs) =
    1.22    let
    1.23      val ts = map (Syntax.check_term ctxt) raw_ts;
    1.24 +    val dTs = map (Syntax.check_typ ctxt) raw_dTs;
    1.25    in
    1.26 -    (fold o fold_aterms)
    1.27 +    []
    1.28 +    |> (fold o fold_aterms)
    1.29        (fn (t as Const (cT as (_, T))) =>
    1.30          if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
    1.31 -        else insert (op =) cT | _ => I) ts []
    1.32 +        else insert (op =) cT | _ => I) ts
    1.33 +    |> fold (fn dT =>
    1.34 +        if not (monomorphic dT) then error ("Polymorphic datatype: " ^ Syntax.string_of_typ ctxt dT)
    1.35 +        else add_all_constrs ctxt dT) dTs
    1.36    end;
    1.37  
    1.38  in
    1.39 @@ -591,9 +609,9 @@
    1.40      val const = Code.check_const thy raw_const;
    1.41    in (print_code ctxt const, register_const const ctxt) end;
    1.42  
    1.43 -fun gen_ml_computation_antiq kind (raw_ts, raw_T) ctxt =
    1.44 +fun gen_ml_computation_antiq kind (raw_T, raw_spec) ctxt =
    1.45    let
    1.46 -    val cTs = prep_terms ctxt raw_ts;
    1.47 +    val cTs = prep_spec ctxt raw_spec;
    1.48      val T = Syntax.check_typ ctxt raw_T;
    1.49      val _ = if not (monomorphic T)
    1.50        then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
    1.51 @@ -604,9 +622,9 @@
    1.52  
    1.53  val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN;
    1.54  
    1.55 -fun ml_computation_check_antiq raw_ts ctxt =
    1.56 +fun ml_computation_check_antiq raw_spec ctxt =
    1.57    let
    1.58 -    val cTs = insert (op =) (dest_Const @{const holds}) (prep_terms ctxt raw_ts);
    1.59 +    val cTs = insert (op =) (dest_Const @{const holds}) (prep_spec ctxt raw_spec);
    1.60    in (print_computation_check ctxt, register_computation cTs @{typ prop} ctxt) end;
    1.61  
    1.62  end; (*local*)
    1.63 @@ -701,25 +719,35 @@
    1.64  
    1.65  (** Isar setup **)
    1.66  
    1.67 +local
    1.68 +
    1.69 +val parse_consts_spec =
    1.70 +  Scan.optional (Scan.lift (Args.$$$ "terms" -- Args.colon) |-- Scan.repeat1 Args.term) []
    1.71 +  -- Scan.optional (Scan.lift (Args.$$$ "datatypes"  -- Args.colon) |-- Scan.repeat1 Args.typ) [];
    1.72 +
    1.73 +in
    1.74 +
    1.75  val _ =
    1.76    Theory.setup (ML_Antiquotation.declaration @{binding code}
    1.77      Args.term (fn _ => ml_code_antiq));
    1.78  
    1.79  val _ =
    1.80    Theory.setup (ML_Antiquotation.declaration @{binding computation}
    1.81 -    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
    1.82 +    (Args.typ -- parse_consts_spec)
    1.83         (fn _ => ml_computation_antiq));
    1.84  
    1.85  val _ =
    1.86    Theory.setup (ML_Antiquotation.declaration @{binding computation_conv}
    1.87 -    (Scan.repeat Args.term --| Scan.lift (Args.$$$ "::") -- Args.typ)
    1.88 +    (Args.typ -- parse_consts_spec)
    1.89         (fn _ => ml_computation_conv_antiq));
    1.90  
    1.91  val _ =
    1.92    Theory.setup (ML_Antiquotation.declaration @{binding computation_check}
    1.93 -    (Scan.repeat Args.term) 
    1.94 +    parse_consts_spec 
    1.95         (fn _ => ml_computation_check_antiq));
    1.96  
    1.97 +end;
    1.98 +
    1.99  local
   1.100  
   1.101  val parse_datatype =