skip abstract constructors silently in datatype clauses of computations
authorhaftmann
Mon Jan 01 20:42:05 2018 +0000 (18 months ago)
changeset 6732789be5a4f514b
parent 67326 17fdb2c98083
child 67328 5ca7bb565ea2
skip abstract constructors silently in datatype clauses of computations
src/Doc/Codegen/Computations.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Doc/Codegen/Computations.thy	Tue Jan 02 21:32:14 2018 +0100
     1.2 +++ b/src/Doc/Codegen/Computations.thy	Mon Jan 01 20:42:05 2018 +0000
     1.3 @@ -131,7 +131,8 @@
     1.4          \<^item> Each type following @{text "datatypes:"} specifies all constructors
     1.5            of the corresponding code datatype as input constants.  Note that
     1.6            this does not increase expressiveness but succinctness for datatypes
     1.7 -          with many constructors.
     1.8 +          with many constructors.  Abstract type constructors are skipped
     1.9 +          silently.
    1.10  
    1.11      \<^item> The code generated by a @{text computation} antiquotation takes a functional argument
    1.12        which describes how to conclude the computation.  What's the rationale
     2.1 --- a/src/Tools/Code/code_runtime.ML	Tue Jan 02 21:32:14 2018 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Jan 01 20:42:05 2018 +0000
     2.3 @@ -598,16 +598,18 @@
     2.4  
     2.5  
     2.6  fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
     2.7 -  let
     2.8 -    val ((vs, constrs), _) = Code.get_type (Proof_Context.theory_of ctxt) tyco;
     2.9 -    val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
    2.10 -    val cs = map (fn (c, (_, Ts')) =>
    2.11 -      (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
    2.12 -        ---> dT)) constrs;
    2.13 -  in
    2.14 -    union (op =) cs
    2.15 -    #> fold (add_all_constrs ctxt) Ts
    2.16 -  end;
    2.17 +  case Code.get_type (Proof_Context.theory_of ctxt) tyco of
    2.18 +    ((vs, constrs), false) =>
    2.19 +      let
    2.20 +        val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
    2.21 +        val cs = map (fn (c, (_, Ts')) =>
    2.22 +          (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
    2.23 +            ---> dT)) constrs;
    2.24 +      in
    2.25 +        union (op =) cs
    2.26 +        #> fold (add_all_constrs ctxt) Ts
    2.27 +      end
    2.28 +  | (_, true) => I;
    2.29  
    2.30  fun prep_spec ctxt (raw_ts, raw_dTs) =
    2.31    let