proper type inference for default values
authorblanchet
Fri Mar 08 14:15:39 2013 +0100 (2013-03-08)
changeset 51380cac8c9a636b6
parent 51379 6dd83e007f56
child 51381 4d691437c076
proper type inference for default values
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Mar 08 13:21:58 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Mar 08 14:15:39 2013 +0100
     1.3 @@ -1165,7 +1165,7 @@
     1.4  
     1.5  val datatypes = define_datatypes (K I) (K I) (K I);
     1.6  
     1.7 -val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
     1.8 +val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
     1.9  
    1.10  val parse_ctr_arg =
    1.11    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
     2.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Mar 08 13:21:58 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Mar 08 14:15:39 2013 +0100
     2.3 @@ -167,7 +167,6 @@
     2.4               SOME disc)) ks ms ctrs0;
     2.5  
     2.6      val no_discs = map is_none disc_bindings;
     2.7 -    val no_discs_at_all = forall I no_discs;
     2.8  
     2.9      fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
    2.10  
    2.11 @@ -240,19 +239,13 @@
    2.12            fun alternate_disc k =
    2.13              Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
    2.14  
    2.15 -          fun mk_default T t =
    2.16 -            let
    2.17 -              val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []);
    2.18 -              val Ts = map TFree (Term.add_tfreesT T []);
    2.19 -            in Term.subst_atomic_types (Ts0 ~~ Ts) t end;
    2.20 -
    2.21            fun mk_sel_case_args b proto_sels T =
    2.22              map2 (fn Ts => fn k =>
    2.23                (case AList.lookup (op =) proto_sels k of
    2.24                  NONE =>
    2.25                  (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
    2.26                    NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
    2.27 -                | SOME t => mk_default (Ts ---> T) t)
    2.28 +                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy)
    2.29                | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
    2.30  
    2.31            fun sel_spec b proto_sels =
    2.32 @@ -658,7 +651,7 @@
    2.33  
    2.34  val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
    2.35    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    2.36 -  prepare_wrap_datatype Syntax.read_term;
    2.37 +  prepare_wrap_datatype Syntax.parse_term;
    2.38  
    2.39  fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    2.40