src/HOL/Tools/Datatype/datatype.ML
author haftmann
Wed Nov 25 11:16:57 2009 +0100 (2009-11-25)
changeset 33959 2afc55e8ed27
parent 33957 e9afca2118d4
child 33963 977b94b64905
permissions -rw-r--r--
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
     1 (*  Title:      HOL/Tools/datatype.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Datatype package for Isabelle/HOL.
     5 *)
     6 
     7 signature DATATYPE =
     8 sig
     9   include DATATYPE_COMMON
    10   val derive_datatype_props : config -> string list -> string list option
    11     -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
    12     -> theory -> string list * theory
    13   val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    14     -> string list option -> term list -> theory -> Proof.state
    15   val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    16   val get_info : theory -> string -> info option
    17   val the_info : theory -> string -> info
    18   val the_descr : theory -> string list
    19     -> descr * (string * sort) list * string list
    20       * string * (string list * string list) * (typ list * typ list)
    21   val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
    22   val all_distincts : theory -> typ list -> thm list list
    23   val get_constrs : theory -> string -> (string * typ) list option
    24   val get_all : theory -> info Symtab.table
    25   val info_of_constr : theory -> string * typ -> info option
    26   val info_of_case : theory -> string -> info option
    27   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
    28   val make_case :  Proof.context -> DatatypeCase.config -> string list -> term ->
    29     (term * term) list -> term * (term * (int * bool)) list
    30   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    31   val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
    32   val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list
    33   val mk_case_names_induct: descr -> attribute
    34   val setup: theory -> theory
    35 end;
    36 
    37 structure Datatype : DATATYPE =
    38 struct
    39 
    40 open DatatypeAux;
    41 
    42 (** theory data **)
    43 
    44 (* data management *)
    45 
    46 structure DatatypesData = Theory_Data
    47 (
    48   type T =
    49     {types: info Symtab.table,
    50      constrs: (string * info) list Symtab.table,
    51      cases: info Symtab.table};
    52 
    53   val empty =
    54     {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
    55   val extend = I;
    56   fun merge
    57     ({types = types1, constrs = constrs1, cases = cases1},
    58      {types = types2, constrs = constrs2, cases = cases2}) : T =
    59     {types = Symtab.merge (K true) (types1, types2),
    60      constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
    61      cases = Symtab.merge (K true) (cases1, cases2)};
    62 );
    63 
    64 val get_all = #types o DatatypesData.get;
    65 val get_info = Symtab.lookup o get_all;
    66 
    67 fun the_info thy name =
    68   (case get_info thy name of
    69     SOME info => info
    70   | NONE => error ("Unknown datatype " ^ quote name));
    71 
    72 fun info_of_constr thy (c, T) =
    73   let
    74     val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
    75     val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE;
    76     val default = if null tab then NONE
    77       else SOME (snd (Library.last_elem tab))
    78         (*conservative wrt. overloaded constructors*);
    79   in case hint
    80    of NONE => default
    81     | SOME tyco => case AList.lookup (op =) tab tyco
    82        of NONE => default (*permissive*)
    83         | SOME info => SOME info
    84   end;
    85 
    86 val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
    87 
    88 fun register (dt_infos : (string * info) list) =
    89   DatatypesData.map (fn {types, constrs, cases} =>
    90     {types = types |> fold Symtab.update dt_infos,
    91      constrs = constrs |> fold (fn (constr, dtname_info) =>
    92          Symtab.map_default (constr, []) (cons dtname_info))
    93        (maps (fn (dtname, info as {descr, index, ...}) =>
    94           map (rpair (dtname, info) o fst)
    95             (#3 (the (AList.lookup op = descr index)))) dt_infos),
    96      cases = cases |> fold Symtab.update
    97        (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
    98 
    99 
   100 (* complex queries *)
   101 
   102 fun the_spec thy dtco =
   103   let
   104     val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
   105     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
   106     val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
   107       o DatatypeAux.dest_DtTFree) dtys;
   108     val cos = map
   109       (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
   110   in (sorts, cos) end;
   111 
   112 fun the_descr thy (raw_tycos as raw_tyco :: _) =
   113   let
   114     val info = the_info thy raw_tyco;
   115     val descr = #descr info;
   116 
   117     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
   118     val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
   119       o dest_DtTFree) dtys;
   120 
   121     fun is_DtTFree (DtTFree _) = true
   122       | is_DtTFree _ = false
   123     val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
   124     val protoTs as (dataTs, _) = chop k descr
   125       |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
   126     
   127     val tycos = map fst dataTs;
   128     val _ = if eq_set (op =) (tycos, raw_tycos) then ()
   129       else error ("Type constructors " ^ commas (map quote raw_tycos)
   130         ^ " do not belong exhaustively to one mutual recursive datatype");
   131 
   132     val (Ts, Us) = (pairself o map) Type protoTs;
   133 
   134     val names = map Long_Name.base_name (the_default tycos (#alt_names info));
   135     val (auxnames, _) = Name.make_context names
   136       |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
   137     val prefix = space_implode "_" names;
   138 
   139   in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
   140 
   141 fun all_distincts thy Ts =
   142   let
   143     fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
   144       | add_tycos _ = I;
   145     val tycos = fold add_tycos Ts [];
   146   in map_filter (Option.map #distinct o get_info thy) tycos end;
   147 
   148 fun get_constrs thy dtco =
   149   case try (the_spec thy) dtco
   150    of SOME (sorts, cos) =>
   151         let
   152           fun subst (v, sort) = TVar ((v, 0), sort);
   153           fun subst_ty (TFree v) = subst v
   154             | subst_ty ty = ty;
   155           val dty = Type (dtco, map subst sorts);
   156           fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
   157         in SOME (map mk_co cos) end
   158     | NONE => NONE;
   159 
   160 
   161 
   162 (** various auxiliary **)
   163 
   164 (* prepare datatype specifications *)
   165 
   166 fun read_typ thy str sorts =
   167   let
   168     val ctxt = ProofContext.init thy
   169       |> fold (Variable.declare_typ o TFree) sorts;
   170     val T = Syntax.read_typ ctxt str;
   171   in (T, Term.add_tfreesT T sorts) end;
   172 
   173 fun cert_typ sign raw_T sorts =
   174   let
   175     val T = Type.no_tvars (Sign.certify_typ sign raw_T)
   176       handle TYPE (msg, _, _) => error msg;
   177     val sorts' = Term.add_tfreesT T sorts;
   178     val _ =
   179       case duplicates (op =) (map fst sorts') of
   180         [] => ()
   181       | dups => error ("Inconsistent sort constraints for " ^ commas dups)
   182   in (T, sorts') end;
   183 
   184 
   185 (* case names *)
   186 
   187 local
   188 
   189 fun dt_recs (DtTFree _) = []
   190   | dt_recs (DtType (_, dts)) = maps dt_recs dts
   191   | dt_recs (DtRec i) = [i];
   192 
   193 fun dt_cases (descr: descr) (_, args, constrs) =
   194   let
   195     fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
   196     val bnames = map the_bname (distinct (op =) (maps dt_recs args));
   197   in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
   198 
   199 fun induct_cases descr =
   200   DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
   201 
   202 fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
   203 
   204 in
   205 
   206 fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
   207 
   208 fun mk_case_names_exhausts descr new =
   209   map (Rule_Cases.case_names o exhaust_cases descr o #1)
   210     (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
   211 
   212 end;
   213 
   214 
   215 (* translation rules for case *)
   216 
   217 fun make_case ctxt = DatatypeCase.make_case
   218   (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
   219 
   220 fun strip_case ctxt = DatatypeCase.strip_case
   221   (info_of_case (ProofContext.theory_of ctxt));
   222 
   223 fun add_case_tr' case_names thy =
   224   Sign.add_advanced_trfuns ([], [],
   225     map (fn case_name =>
   226       let val case_name' = Sign.const_syntax_name thy case_name
   227       in (case_name', DatatypeCase.case_tr' info_of_case case_name')
   228       end) case_names, []) thy;
   229 
   230 val trfun_setup =
   231   Sign.add_advanced_trfuns ([],
   232     [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
   233     [], []);
   234 
   235 
   236 
   237 (** document antiquotation **)
   238 
   239 val _ = ThyOutput.antiquotation "datatype" Args.tyname
   240   (fn {source = src, context = ctxt, ...} => fn dtco =>
   241     let
   242       val thy = ProofContext.theory_of ctxt;
   243       val (vs, cos) = the_spec thy dtco;
   244       val ty = Type (dtco, map TFree vs);
   245       fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
   246             Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
   247         | pretty_typ_bracket ty =
   248             Syntax.pretty_typ ctxt ty;
   249       fun pretty_constr (co, tys) =
   250         (Pretty.block o Pretty.breaks)
   251           (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
   252             map pretty_typ_bracket tys);
   253       val pretty_datatype =
   254         Pretty.block
   255           (Pretty.command "datatype" :: Pretty.brk 1 ::
   256            Syntax.pretty_typ ctxt ty ::
   257            Pretty.str " =" :: Pretty.brk 1 ::
   258            flat (separate [Pretty.brk 1, Pretty.str "| "]
   259              (map (single o pretty_constr) cos)));
   260     in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
   261 
   262 
   263 
   264 (** abstract theory extensions relative to a datatype characterisation **)
   265 
   266 structure Datatype_Interpretation = Interpretation
   267   (type T = config * string list val eq: T * T -> bool = eq_snd op =);
   268 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
   269 
   270 fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
   271     (index, (((((((((((_, (tname, _, _))), inject), distinct),
   272       exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
   273         (split, split_asm))) =
   274   (tname,
   275    {index = index,
   276     alt_names = alt_names,
   277     descr = descr,
   278     sorts = sorts,
   279     inject = inject,
   280     distinct = distinct,
   281     induct = induct,
   282     inducts = inducts,
   283     exhaust = exhaust,
   284     nchotomy = nchotomy,
   285     rec_names = rec_names,
   286     rec_rewrites = rec_rewrites,
   287     case_name = case_name,
   288     case_rewrites = case_rewrites,
   289     case_cong = case_cong,
   290     weak_case_cong = weak_case_cong,
   291     split = split,
   292     split_asm = split_asm});
   293 
   294 fun derive_datatype_props config dt_names alt_names descr sorts
   295     induct inject distinct thy1 =
   296   let
   297     val thy2 = thy1 |> Theory.checkpoint;
   298     val flat_descr = flat descr;
   299     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
   300     val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
   301 
   302     val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
   303       descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
   304     val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   305       descr sorts exhaust thy3;
   306     val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
   307       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
   308       inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
   309       induct thy4;
   310     val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   311       config new_type_names descr sorts rec_names rec_rewrites thy5;
   312     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
   313       descr sorts nchotomys case_rewrites thy6;
   314     val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   315       descr sorts thy7;
   316     val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
   317       config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
   318 
   319     val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
   320     val dt_infos = map_index
   321       (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
   322       (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
   323         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
   324     val dt_names = map fst dt_infos;
   325     val prfx = Binding.qualify true (space_implode "_" new_type_names);
   326     val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
   327     val named_rules = flat (map_index (fn (index, tname) =>
   328       [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
   329        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
   330     val unnamed_rules = map (fn induct =>
   331       ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
   332         (drop (length dt_names) inducts);
   333   in
   334     thy9
   335     |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
   336         ((prfx (Binding.name "inducts"), inducts), []),
   337         ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
   338         ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
   339           [Simplifier.simp_add]),
   340         ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
   341         ((Binding.empty, flat inject), [iff_add]),
   342         ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
   343           [Classical.safe_elim NONE]),
   344         ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
   345         @ named_rules @ unnamed_rules)
   346     |> snd
   347     |> add_case_tr' case_names
   348     |> register dt_infos
   349     |> Datatype_Interpretation.data (config, dt_names)
   350     |> pair dt_names
   351   end;
   352 
   353 
   354 
   355 (** declare existing type as datatype **)
   356 
   357 fun prove_rep_datatype config dt_names alt_names descr sorts
   358     raw_inject half_distinct raw_induct thy1 =
   359   let
   360     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
   361     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
   362     val (((inject, distinct), [induct]), thy2) =
   363       thy1
   364       |> store_thmss "inject" new_type_names raw_inject
   365       ||>> store_thmss "distinct" new_type_names raw_distinct
   366       ||> Sign.add_path (space_implode "_" new_type_names)
   367       ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
   368       ||> Sign.restore_naming thy1;
   369   in
   370     thy2
   371     |> derive_datatype_props config dt_names alt_names [descr] sorts
   372          induct inject distinct
   373  end;
   374 
   375 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
   376   let
   377     fun constr_of_term (Const (c, T)) = (c, T)
   378       | constr_of_term t =
   379           error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   380     fun no_constr (c, T) = error ("Bad constructor: "
   381       ^ Sign.extern_const thy c ^ "::"
   382       ^ Syntax.string_of_typ_global thy T);
   383     fun type_of_constr (cT as (_, T)) =
   384       let
   385         val frees = OldTerm.typ_tfrees T;
   386         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
   387           handle TYPE _ => no_constr cT
   388         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
   389         val _ = if length frees <> length vs then no_constr cT else ();
   390       in (tyco, (vs, cT)) end;
   391 
   392     val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
   393     val _ = case map_filter (fn (tyco, _) =>
   394         if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
   395      of [] => ()
   396       | tycos => error ("Type(s) " ^ commas (map quote tycos)
   397           ^ " already represented inductivly");
   398     val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
   399     val ms = case distinct (op =) (map length raw_vss)
   400      of [n] => 0 upto n - 1
   401       | _ => error ("Different types in given constructors");
   402     fun inter_sort m = map (fn xs => nth xs m) raw_vss
   403       |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   404     val sorts = map inter_sort ms;
   405     val vs = Name.names Name.context Name.aT sorts;
   406 
   407     fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
   408       (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
   409 
   410     val cs = map (apsnd (map norm_constr)) raw_cs;
   411     val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
   412       o fst o strip_type;
   413     val dt_names = map fst cs;
   414 
   415     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
   416       map (DtTFree o fst) vs,
   417       (map o apsnd) dtyps_of_typ constr))
   418     val descr = map_index mk_spec cs;
   419     val injs = DatatypeProp.make_injs [descr] vs;
   420     val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
   421     val ind = DatatypeProp.make_ind [descr] vs;
   422     val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
   423 
   424     fun after_qed' raw_thms =
   425       let
   426         val [[[raw_induct]], raw_inject, half_distinct] =
   427           unflat rules (map Drule.zero_var_indexes_list raw_thms);
   428             (*FIXME somehow dubious*)
   429       in
   430         ProofContext.theory_result
   431           (prove_rep_datatype config dt_names alt_names descr vs
   432             raw_inject half_distinct raw_induct)
   433         #-> after_qed
   434       end;
   435   in
   436     thy
   437     |> ProofContext.init
   438     |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
   439   end;
   440 
   441 val rep_datatype = gen_rep_datatype Sign.cert_term;
   442 val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
   443 
   444 
   445 
   446 (** package setup **)
   447 
   448 (* setup theory *)
   449 
   450 val setup =
   451   trfun_setup #>
   452   Datatype_Interpretation.init;
   453 
   454 
   455 (* outer syntax *)
   456 
   457 local
   458 
   459 structure P = OuterParse and K = OuterKeyword
   460 
   461 in
   462 
   463 val _ =
   464   OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
   465     (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
   466       >> (fn (alt_names, ts) => Toplevel.print
   467            o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
   468 
   469 end;
   470 
   471 end;