new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
authorkrauss
Mon Jun 27 17:04:04 2011 +0200 (2011-06-27)
changeset 43580023a1d1f97bd
parent 43579 66f8cf4f82d9
child 43581 c3e4d280bdeb
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
renamed old version to info_of_constr_permissive, reflecting its semantics
src/HOL/Inductive.thy
src/HOL/List.thy
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Inductive.thy	Mon Jun 27 14:56:39 2011 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Mon Jun 27 17:04:04 2011 +0200
     1.3 @@ -297,7 +297,7 @@
     1.4      let
     1.5        (* FIXME proper name context!? *)
     1.6        val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
     1.7 -      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
     1.8 +      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs];
     1.9      in lambda x ft end
    1.10  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.11  *}
     2.1 --- a/src/HOL/List.thy	Mon Jun 27 14:56:39 2011 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Jun 27 17:04:04 2011 +0200
     2.3 @@ -391,7 +391,7 @@
     2.4          Syntax.const @{syntax_const "_case1"} $
     2.5            Syntax.const @{const_syntax dummy_pattern} $ NilC;
     2.6        val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
     2.7 -      val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
     2.8 +      val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs];
     2.9      in lambda x ft end;
    2.10  
    2.11    fun abs_tr ctxt (p as Free (s, T)) e opti =
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jun 27 14:56:39 2011 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jun 27 17:04:04 2011 +0200
     3.3 @@ -23,6 +23,7 @@
     3.4    val get_constrs : theory -> string -> (string * typ) list option
     3.5    val get_all : theory -> info Symtab.table
     3.6    val info_of_constr : theory -> string * typ -> info option
     3.7 +  val info_of_constr_permissive : theory -> string * typ -> info option
     3.8    val info_of_case : theory -> string -> info option
     3.9    val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
    3.10    val make_case :  Proof.context -> Datatype_Case.config -> string list -> term ->
    3.11 @@ -70,6 +71,15 @@
    3.12  fun info_of_constr thy (c, T) =
    3.13    let
    3.14      val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
    3.15 +  in
    3.16 +    case body_type T of
    3.17 +      Type (tyco, _) => AList.lookup (op =) tab tyco
    3.18 +    | _ => NONE
    3.19 +  end;
    3.20 +
    3.21 +fun info_of_constr_permissive thy (c, T) =
    3.22 +  let
    3.23 +    val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
    3.24      val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
    3.25      val default =
    3.26        if null tab then NONE
    3.27 @@ -216,7 +226,7 @@
    3.28  (* translation rules for case *)
    3.29  
    3.30  fun make_case ctxt = Datatype_Case.make_case
    3.31 -  (info_of_constr (Proof_Context.theory_of ctxt)) ctxt;
    3.32 +  (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
    3.33  
    3.34  fun strip_case ctxt = Datatype_Case.strip_case
    3.35    (info_of_case (Proof_Context.theory_of ctxt));
    3.36 @@ -230,7 +240,7 @@
    3.37  
    3.38  val trfun_setup =
    3.39    Sign.add_advanced_trfuns ([],
    3.40 -    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr)],
    3.41 +    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)],
    3.42      [], []);
    3.43  
    3.44