towards support for HO SMT-LIB
authorblanchet
Tue Aug 29 18:30:23 2017 +0200 (22 months ago)
changeset 665514df6b0ae900d
parent 66550 e5d82cf3c387
child 66553 6ab32ffb2bdd
towards support for HO SMT-LIB
src/HOL/SMT.thy
src/HOL/Tools/SMT/cvc4_interface.ML
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smt_util.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Word/Tools/smt_word.ML
     1.1 --- a/src/HOL/SMT.thy	Tue Aug 29 16:24:14 2017 +0200
     1.2 +++ b/src/HOL/SMT.thy	Tue Aug 29 18:30:23 2017 +0200
     1.3 @@ -1,12 +1,13 @@
     1.4  (*  Title:      HOL/SMT.thy
     1.5      Author:     Sascha Boehme, TU Muenchen
     1.6 +    Author:     Jasmin Blanchette, VU Amsterdam
     1.7  *)
     1.8  
     1.9  section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
    1.10  
    1.11  theory SMT
    1.12 -imports Divides
    1.13 -keywords "smt_status" :: diag
    1.14 +  imports Divides
    1.15 +  keywords "smt_status" :: diag
    1.16  begin
    1.17  
    1.18  subsection \<open>A skolemization tactic and proof method\<close>
     2.1 --- a/src/HOL/Tools/SMT/cvc4_interface.ML	Tue Aug 29 16:24:14 2017 +0200
     2.2 +++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Tue Aug 29 18:30:23 2017 +0200
     2.3 @@ -7,24 +7,30 @@
     2.4  signature CVC4_INTERFACE =
     2.5  sig
     2.6    val smtlib_cvc4C: SMT_Util.class
     2.7 +  val hosmtlib_cvc4C: SMT_Util.class
     2.8  end;
     2.9  
    2.10  structure CVC4_Interface: CVC4_INTERFACE =
    2.11  struct
    2.12  
    2.13 -val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
    2.14 +val cvc4C = ["cvc4"]
    2.15 +val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
    2.16 +val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
    2.17  
    2.18  
    2.19  (* interface *)
    2.20  
    2.21  local
    2.22 -  fun translate_config ctxt =
    2.23 -    {logic = K "(set-logic ALL_SUPPORTED)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
    2.24 -     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
    2.25 +  fun translate_config order ctxt =
    2.26 +    {order = order,
    2.27 +     logic = K "(set-logic ALL_SUPPORTED)\n",
    2.28 +     fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
    2.29 +     serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
    2.30  in
    2.31  
    2.32 -val _ =
    2.33 -  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
    2.34 +val _ = Theory.setup (Context.theory_map
    2.35 +  (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
    2.36 +   SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
    2.37  
    2.38  end
    2.39  
     3.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Aug 29 16:24:14 2017 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Aug 29 18:30:23 2017 +0200
     3.3 @@ -11,11 +11,11 @@
     3.4  
     3.5    (*built-in types*)
     3.6    val add_builtin_typ: SMT_Util.class ->
     3.7 -    typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
     3.8 +    typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
     3.9      Context.generic
    3.10    val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
    3.11      Context.generic
    3.12 -  val dest_builtin_typ: Proof.context -> typ -> string option
    3.13 +  val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
    3.14    val is_builtin_typ_ext: Proof.context -> typ -> bool
    3.15  
    3.16    (*built-in numbers*)
    3.17 @@ -93,7 +93,8 @@
    3.18  structure Builtins = Generic_Data
    3.19  (
    3.20    type T =
    3.21 -    (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
    3.22 +    (Proof.context -> typ -> bool,
    3.23 +     (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
    3.24      (term list bfun, bfunr option bfun) btab
    3.25    val empty = ([], Symtab.empty)
    3.26    val extend = I
     4.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Aug 29 16:24:14 2017 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Aug 29 18:30:23 2017 +0200
     4.3 @@ -32,6 +32,7 @@
     4.4    val statistics: bool Config.T
     4.5    val monomorph_limit: int Config.T
     4.6    val monomorph_instances: int Config.T
     4.7 +  val higher_order: bool Config.T
     4.8    val nat_as_int: bool Config.T
     4.9    val infer_triggers: bool Config.T
    4.10    val debug_files: string Config.T
    4.11 @@ -180,6 +181,7 @@
    4.12  val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
    4.13  val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    4.14  val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    4.15 +val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
    4.16  val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
    4.17  val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
    4.18  val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
     5.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Tue Aug 29 16:24:14 2017 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Aug 29 18:30:23 2017 +0200
     5.3 @@ -32,7 +32,7 @@
     5.4  
     5.5  val setup_builtins =
     5.6    SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
     5.7 -    (@{typ real}, K (SOME "Real"), real_num) #>
     5.8 +    (@{typ real}, K (SOME ("Real", [])), real_num) #>
     5.9    fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
    5.10      (@{const less (real)}, "<"),
    5.11      (@{const less_eq (real)}, "<="),
     6.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Tue Aug 29 16:24:14 2017 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Tue Aug 29 18:30:23 2017 +0200
     6.3 @@ -62,6 +62,7 @@
     6.4  
     6.5  end
     6.6  
     6.7 +
     6.8  (* CVC4 *)
     6.9  
    6.10  val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
    6.11 @@ -75,8 +76,16 @@
    6.12      "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
    6.13  
    6.14    fun select_class ctxt =
    6.15 -    if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
    6.16 -    else SMTLIB_Interface.smtlibC
    6.17 +    if Config.get ctxt cvc4_extensions then
    6.18 +      if Config.get ctxt SMT_Config.higher_order then
    6.19 +        CVC4_Interface.hosmtlib_cvc4C
    6.20 +      else
    6.21 +        CVC4_Interface.smtlib_cvc4C
    6.22 +    else
    6.23 +      if Config.get ctxt SMT_Config.higher_order then
    6.24 +        SMTLIB_Interface.hosmtlibC
    6.25 +      else
    6.26 +        SMTLIB_Interface.smtlibC
    6.27  in
    6.28  
    6.29  val cvc4: SMT_Solver.solver_config = {
    6.30 @@ -93,11 +102,20 @@
    6.31  
    6.32  end
    6.33  
    6.34 +
    6.35  (* veriT *)
    6.36  
    6.37 +local
    6.38 +  fun select_class ctxt =
    6.39 +    if Config.get ctxt SMT_Config.higher_order then
    6.40 +      SMTLIB_Interface.hosmtlibC
    6.41 +    else
    6.42 +      SMTLIB_Interface.smtlibC
    6.43 +in
    6.44 +
    6.45  val veriT: SMT_Solver.solver_config = {
    6.46    name = "verit",
    6.47 -  class = K SMTLIB_Interface.smtlibC,
    6.48 +  class = select_class,
    6.49    avail = make_avail "VERIT",
    6.50    command = make_command "VERIT",
    6.51    options = (fn ctxt => [
    6.52 @@ -113,6 +131,9 @@
    6.53    parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
    6.54    replay = NONE }
    6.55  
    6.56 +end
    6.57 +
    6.58 +
    6.59  (* Z3 *)
    6.60  
    6.61  val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
     7.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Aug 29 16:24:14 2017 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Aug 29 18:30:23 2017 +0200
     7.3 @@ -10,8 +10,8 @@
     7.4    datatype squant = SForall | SExists
     7.5    datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
     7.6    datatype sterm =
     7.7 -    SVar of int |
     7.8 -    SApp of string * sterm list |
     7.9 +    SVar of int * sterm list |
    7.10 +    SConst of string * sterm list |
    7.11      SQua of squant * string list * sterm spattern list * sterm
    7.12  
    7.13    (*translation configuration*)
    7.14 @@ -21,6 +21,7 @@
    7.15      dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
    7.16      funcs: (string * (string list * string)) list }
    7.17    type config = {
    7.18 +    order: SMT_Util.order,
    7.19      logic: term list -> string,
    7.20      fp_kinds: BNF_Util.fp_kind list,
    7.21      serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    7.22 @@ -50,8 +51,8 @@
    7.23    SPat of 'a list | SNoPat of 'a list
    7.24  
    7.25  datatype sterm =
    7.26 -  SVar of int |
    7.27 -  SApp of string * sterm list |
    7.28 +  SVar of int * sterm list |
    7.29 +  SConst of string * sterm list |
    7.30    SQua of squant * string list * sterm spattern list * sterm
    7.31  
    7.32  
    7.33 @@ -64,6 +65,7 @@
    7.34    funcs: (string * (string list * string)) list }
    7.35  
    7.36  type config = {
    7.37 +  order: SMT_Util.order,
    7.38    logic: term list -> string,
    7.39    fp_kinds: BNF_Util.fp_kind list,
    7.40    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    7.41 @@ -147,7 +149,7 @@
    7.42  
    7.43      fun add_typ' T proper =
    7.44        (case SMT_Builtin.dest_builtin_typ ctxt' T of
    7.45 -        SOME n => pair n
    7.46 +        SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
    7.47        | NONE => add_typ T proper)
    7.48  
    7.49      fun tr_select sel =
    7.50 @@ -425,11 +427,12 @@
    7.51        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
    7.52        | transT (T as Type _) =
    7.53            (case SMT_Builtin.dest_builtin_typ ctxt T of
    7.54 -            SOME n => pair n
    7.55 +            SOME (n, []) => pair n
    7.56 +          | SOME (n, Ts) =>
    7.57 +            fold_map transT Ts
    7.58 +            #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
    7.59            | NONE => add_typ T true)
    7.60  
    7.61 -    fun app n ts = SApp (n, ts)
    7.62 -
    7.63      fun trans t =
    7.64        (case Term.strip_comb t of
    7.65          (Const (qn, _), [Abs (_, T, t1)]) =>
    7.66 @@ -440,17 +443,17 @@
    7.67            | NONE => raise TERM ("unsupported quantifier", [t]))
    7.68        | (u as Const (c as (_, T)), ts) =>
    7.69            (case builtin ctxt c ts of
    7.70 -            SOME (n, _, us, _) => fold_map trans us #>> app n
    7.71 -          | NONE => transs u T ts)
    7.72 -      | (u as Free (_, T), ts) => transs u T ts
    7.73 -      | (Bound i, []) => pair (SVar i)
    7.74 +            SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
    7.75 +          | NONE => trans_applied_fun u T ts)
    7.76 +      | (u as Free (_, T), ts) => trans_applied_fun u T ts
    7.77 +      | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
    7.78        | _ => raise TERM ("bad SMT term", [t]))
    7.79  
    7.80 -    and transs t T ts =
    7.81 +    and trans_applied_fun t T ts =
    7.82        let val (Us, U) = SMT_Util.dest_funT (length ts) T
    7.83        in
    7.84          fold_map transT Us ##>> transT U #-> (fn Up =>
    7.85 -          add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
    7.86 +          add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
    7.87        end
    7.88  
    7.89      val (us, trx') = fold_map trans ts trx
    7.90 @@ -480,7 +483,7 @@
    7.91  
    7.92  fun translate ctxt smt_options comments ithms =
    7.93    let
    7.94 -    val {logic, fp_kinds, serialize} = get_config ctxt
    7.95 +    val {order, logic, fp_kinds, serialize} = get_config ctxt
    7.96  
    7.97      fun no_dtyps (tr_context, ctxt) ts =
    7.98        ((Termtab.empty, [], tr_context, ctxt), ts)
    7.99 @@ -510,10 +513,14 @@
   7.100        |> rpair ctxt1
   7.101        |-> Lambda_Lifting.lift_lambdas NONE is_binder
   7.102        |-> (fn (ts', ll_defs) => fn ctxt' =>
   7.103 -          (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
   7.104 -
   7.105 +        let
   7.106 +          val ts'' = map mk_trigger ll_defs @ ts'
   7.107 +            |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
   7.108 +        in
   7.109 +          (ctxt', (ts'', ll_defs))
   7.110 +        end)
   7.111      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
   7.112 -      |>> apfst (cons fun_app_eq)
   7.113 +      |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
   7.114    in
   7.115      (ts4, tr_context)
   7.116      |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
     8.1 --- a/src/HOL/Tools/SMT/smt_util.ML	Tue Aug 29 16:24:14 2017 +0200
     8.2 +++ b/src/HOL/Tools/SMT/smt_util.ML	Tue Aug 29 18:30:23 2017 +0200
     8.3 @@ -10,6 +10,8 @@
     8.4    val repeat: ('a -> 'a option) -> 'a -> 'a
     8.5    val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
     8.6  
     8.7 +  datatype order = First_Order | Higher_Order
     8.8 +
     8.9    (*class dictionaries*)
    8.10    type class = string list
    8.11    val basicC: class
    8.12 @@ -79,6 +81,11 @@
    8.13    in rep end
    8.14  
    8.15  
    8.16 +(* order *)
    8.17 +
    8.18 +datatype order = First_Order | Higher_Order
    8.19 +
    8.20 +
    8.21  (* class dictionaries *)
    8.22  
    8.23  type class = string list
     9.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Aug 29 16:24:14 2017 +0200
     9.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Aug 29 18:30:23 2017 +0200
     9.3 @@ -8,8 +8,9 @@
     9.4  signature SMTLIB_INTERFACE =
     9.5  sig
     9.6    val smtlibC: SMT_Util.class
     9.7 +  val hosmtlibC: SMT_Util.class
     9.8    val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
     9.9 -  val translate_config: Proof.context -> SMT_Translate.config
    9.10 +  val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
    9.11    val assert_name_of_index: int -> string
    9.12    val assert_index_of_name: string -> int
    9.13    val assert_prefix : string
    9.14 @@ -18,7 +19,10 @@
    9.15  structure SMTLIB_Interface: SMTLIB_INTERFACE =
    9.16  struct
    9.17  
    9.18 -val smtlibC = ["smtlib"]
    9.19 +val hoC = ["ho"]
    9.20 +
    9.21 +val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
    9.22 +val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
    9.23  
    9.24  
    9.25  (* builtins *)
    9.26 @@ -36,9 +40,11 @@
    9.27  in
    9.28  
    9.29  val setup_builtins =
    9.30 +  SMT_Builtin.add_builtin_typ hosmtlibC
    9.31 +    (@{typ "'a => 'b"}, fn Type (@{type_name fun}, Ts) => SOME ("->", Ts), K (K NONE)) #>
    9.32    fold (SMT_Builtin.add_builtin_typ smtlibC) [
    9.33 -    (@{typ bool}, K (SOME "Bool"), K (K NONE)),
    9.34 -    (@{typ int}, K (SOME "Int"), int_num)] #>
    9.35 +    (@{typ bool}, K (SOME ("Bool", [])), K (K NONE)),
    9.36 +    (@{typ int}, K (SOME ("Int", [])), int_num)] #>
    9.37    fold (SMT_Builtin.add_builtin_fun' smtlibC) [
    9.38      (@{const True}, "true"),
    9.39      (@{const False}, "false"),
    9.40 @@ -90,9 +96,11 @@
    9.41  
    9.42  fun var i = "?v" ^ string_of_int i
    9.43  
    9.44 -fun tree_of_sterm l (SMT_Translate.SVar i) = SMTLIB.Sym (var (l - i - 1))
    9.45 -  | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
    9.46 -  | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
    9.47 +fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
    9.48 +  | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
    9.49 +      SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
    9.50 +  | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
    9.51 +  | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
    9.52        SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
    9.53    | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
    9.54        let
    9.55 @@ -157,13 +165,15 @@
    9.56  
    9.57  (* interface *)
    9.58  
    9.59 -fun translate_config ctxt = {
    9.60 +fun translate_config order ctxt = {
    9.61 +  order = order,
    9.62    logic = choose_logic ctxt,
    9.63    fp_kinds = [],
    9.64    serialize = serialize}
    9.65  
    9.66  val _ = Theory.setup (Context.theory_map
    9.67    (setup_builtins #>
    9.68 -   SMT_Translate.add_config (smtlibC, translate_config)))
    9.69 +   SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
    9.70 +   SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
    9.71  
    9.72  end;
    10.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Aug 29 16:24:14 2017 +0200
    10.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Aug 29 18:30:23 2017 +0200
    10.3 @@ -24,15 +24,19 @@
    10.4  structure Z3_Interface: Z3_INTERFACE =
    10.5  struct
    10.6  
    10.7 -val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
    10.8 +val z3C = ["z3"]
    10.9 +
   10.10 +val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
   10.11  
   10.12  
   10.13  (* interface *)
   10.14  
   10.15  local
   10.16    fun translate_config ctxt =
   10.17 -    {logic = K "", fp_kinds = [BNF_Util.Least_FP],
   10.18 -     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
   10.19 +    {order = SMT_Util.First_Order,
   10.20 +     logic = K "",
   10.21 +     fp_kinds = [BNF_Util.Least_FP],
   10.22 +     serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
   10.23  
   10.24    fun is_div_mod @{const divide (int)} = true
   10.25      | is_div_mod @{const modulo (int)} = true
    11.1 --- a/src/HOL/Word/Tools/smt_word.ML	Tue Aug 29 16:24:14 2017 +0200
    11.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Tue Aug 29 18:30:23 2017 +0200
    11.3 @@ -28,7 +28,8 @@
    11.4    fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
    11.5    fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
    11.6  
    11.7 -  fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T)
    11.8 +  fun word_typ (Type (@{type_name word}, [T])) =
    11.9 +      Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
   11.10      | word_typ _ = NONE
   11.11  
   11.12    fun word_num (Type (@{type_name word}, [T])) k =