src/HOL/Tools/Datatype/datatype_codegen.ML
author haftmann
Tue Nov 24 17:28:25 2009 +0100 (2009-11-24)
changeset 33955 fff6f11b1f09
parent 33553 35f2b30593a8
child 33957 e9afca2118d4
permissions -rw-r--r--
curried take/drop
     1 (*  Title:      HOL/Tools/datatype_codegen.ML
     2     Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
     3 
     4 Code generator facilities for inductive datatypes.
     5 *)
     6 
     7 signature DATATYPE_CODEGEN =
     8 sig
     9   val find_shortest_path: Datatype.descr -> int -> (string * int) option
    10   val setup: theory -> theory
    11 end;
    12 
    13 structure DatatypeCodegen : DATATYPE_CODEGEN =
    14 struct
    15 
    16 (** find shortest path to constructor with no recursive arguments **)
    17 
    18 fun find_nonempty (descr: Datatype.descr) is i =
    19   let
    20     val (_, _, constrs) = the (AList.lookup (op =) descr i);
    21     fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
    22           then NONE
    23           else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
    24       | arg_nonempty _ = SOME 0;
    25     fun max xs = Library.foldl
    26       (fn (NONE, _) => NONE
    27         | (SOME i, SOME j) => SOME (Int.max (i, j))
    28         | (_, NONE) => NONE) (SOME 0, xs);
    29     val xs = sort (int_ord o pairself snd)
    30       (map_filter (fn (s, dts) => Option.map (pair s)
    31         (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
    32   in case xs of [] => NONE | x :: _ => SOME x end;
    33 
    34 fun find_shortest_path descr i = find_nonempty descr [i] i;
    35 
    36 
    37 (** SML code generator **)
    38 
    39 open Codegen;
    40 
    41 (* datatype definition *)
    42 
    43 fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
    44   let
    45     val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    46     val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
    47       exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
    48 
    49     val (_, (tname, _, _)) :: _ = descr';
    50     val node_id = tname ^ " (type)";
    51     val module' = if_library (thyname_of_type thy tname) module;
    52 
    53     fun mk_dtdef prfx [] gr = ([], gr)
    54       | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
    55           let
    56             val tvs = map DatatypeAux.dest_DtTFree dts;
    57             val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    58             val ((_, type_id), gr') = mk_type_id module' tname gr;
    59             val (ps, gr'') = gr' |>
    60               fold_map (fn (cname, cargs) =>
    61                 fold_map (invoke_tycodegen thy defs node_id module' false)
    62                   cargs ##>>
    63                 mk_const_id module' cname) cs';
    64             val (rest, gr''') = mk_dtdef "and " xs gr''
    65           in
    66             (Pretty.block (str prfx ::
    67                (if null tvs then [] else
    68                   [mk_tuple (map str tvs), str " "]) @
    69                [str (type_id ^ " ="), Pretty.brk 1] @
    70                flat (separate [Pretty.brk 1, str "| "]
    71                  (map (fn (ps', (_, cname)) => [Pretty.block
    72                    (str cname ::
    73                     (if null ps' then [] else
    74                      flat ([str " of", Pretty.brk 1] ::
    75                        separate [str " *", Pretty.brk 1]
    76                          (map single ps'))))]) ps))) :: rest, gr''')
    77           end;
    78 
    79     fun mk_constr_term cname Ts T ps =
    80       flat (separate [str " $", Pretty.brk 1]
    81         ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    82           mk_type false (Ts ---> T), str ")"] :: ps));
    83 
    84     fun mk_term_of_def gr prfx [] = []
    85       | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
    86           let
    87             val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    88             val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
    89             val T = Type (tname, dts');
    90             val rest = mk_term_of_def gr "and " xs;
    91             val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
    92               let val args = map (fn i =>
    93                 str ("x" ^ string_of_int i)) (1 upto length Ts)
    94               in (Pretty.blk (4,
    95                 [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    96                  if null Ts then str (snd (get_const_id gr cname))
    97                  else parens (Pretty.block
    98                    [str (snd (get_const_id gr cname)),
    99                     Pretty.brk 1, mk_tuple args]),
   100                  str " =", Pretty.brk 1] @
   101                  mk_constr_term cname Ts T
   102                    (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U,
   103                       Pretty.brk 1, x]]) args Ts)), "  | ")
   104               end) cs' prfx
   105           in eqs @ rest end;
   106 
   107     fun mk_gen_of_def gr prfx [] = []
   108       | mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) =
   109           let
   110             val tvs = map DatatypeAux.dest_DtTFree dts;
   111             val Us = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
   112             val T = Type (tname, Us);
   113             val (cs1, cs2) =
   114               List.partition (exists DatatypeAux.is_rec_type o snd) cs;
   115             val SOME (cname, _) = find_shortest_path descr i;
   116 
   117             fun mk_delay p = Pretty.block
   118               [str "fn () =>", Pretty.brk 1, p];
   119 
   120             fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"];
   121 
   122             fun mk_constr s b (cname, dts) =
   123               let
   124                 val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
   125                     (DatatypeAux.typ_of_dtyp descr sorts dt))
   126                   [str (if b andalso DatatypeAux.is_rec_type dt then "0"
   127                      else "j")]) dts;
   128                 val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
   129                 val xs = map str
   130                   (DatatypeProp.indexify_names (replicate (length dts) "x"));
   131                 val ts = map str
   132                   (DatatypeProp.indexify_names (replicate (length dts) "t"));
   133                 val (_, id) = get_const_id gr cname
   134               in
   135                 mk_let
   136                   (map2 (fn p => fn q => mk_tuple [p, q]) xs ts ~~ gs)
   137                   (mk_tuple
   138                     [case xs of
   139                        _ :: _ :: _ => Pretty.block
   140                          [str id, Pretty.brk 1, mk_tuple xs]
   141                      | _ => mk_app false (str id) xs,
   142                      mk_delay (Pretty.block (mk_constr_term cname Ts T
   143                        (map (single o mk_force) ts)))])
   144               end;
   145 
   146             fun mk_choice [c] = mk_constr "(i-1)" false c
   147               | mk_choice cs = Pretty.block [str "one_of",
   148                   Pretty.brk 1, Pretty.blk (1, str "[" ::
   149                   flat (separate [str ",", Pretty.fbrk]
   150                     (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
   151                   [str "]"]), Pretty.brk 1, str "()"];
   152 
   153             val gs = maps (fn s =>
   154               let val s' = strip_tname s
   155               in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
   156             val gen_name = "gen_" ^ snd (get_type_id gr tname)
   157 
   158           in
   159             Pretty.blk (4, separate (Pretty.brk 1) 
   160                 (str (prfx ^ gen_name ^
   161                    (if null cs1 then "" else "'")) :: gs @
   162                  (if null cs1 then [] else [str "i"]) @
   163                  [str "j"]) @
   164               [str " =", Pretty.brk 1] @
   165               (if not (null cs1) andalso not (null cs2)
   166                then [str "frequency", Pretty.brk 1,
   167                  Pretty.blk (1, [str "[",
   168                    mk_tuple [str "i", mk_delay (mk_choice cs1)],
   169                    str ",", Pretty.fbrk,
   170                    mk_tuple [str "1", mk_delay (mk_choice cs2)],
   171                    str "]"]), Pretty.brk 1, str "()"]
   172                else if null cs2 then
   173                  [Pretty.block [str "(case", Pretty.brk 1,
   174                    str "i", Pretty.brk 1, str "of",
   175                    Pretty.brk 1, str "0 =>", Pretty.brk 1,
   176                    mk_constr "0" true (cname, the (AList.lookup (op =) cs cname)),
   177                    Pretty.brk 1, str "| _ =>", Pretty.brk 1,
   178                    mk_choice cs1, str ")"]]
   179                else [mk_choice cs2])) ::
   180             (if null cs1 then []
   181              else [Pretty.blk (4, separate (Pretty.brk 1) 
   182                  (str ("and " ^ gen_name) :: gs @ [str "i"]) @
   183                [str " =", Pretty.brk 1] @
   184                separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @
   185                  [str "i", str "i"]))]) @
   186             mk_gen_of_def gr "and " xs
   187           end
   188 
   189   in
   190     (module', (add_edge_acyclic (node_id, dep) gr
   191         handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
   192          let
   193            val gr1 = add_edge (node_id, dep)
   194              (new_node (node_id, (NONE, "", "")) gr);
   195            val (dtdef, gr2) = mk_dtdef "datatype " descr' gr1 ;
   196          in
   197            map_node node_id (K (NONE, module',
   198              string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   199                [str ";"])) ^ "\n\n" ^
   200              (if "term_of" mem !mode then
   201                 string_of (Pretty.blk (0, separate Pretty.fbrk
   202                   (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   203               else "") ^
   204              (if "test" mem !mode then
   205                 string_of (Pretty.blk (0, separate Pretty.fbrk
   206                   (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   207               else ""))) gr2
   208          end)
   209   end;
   210 
   211 
   212 (* case expressions *)
   213 
   214 fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
   215   let val i = length constrs
   216   in if length ts <= i then
   217        invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
   218     else
   219       let
   220         val ts1 = (uncurry take) (i, ts);
   221         val t :: ts2 = (uncurry drop) (i, ts);
   222         val names = List.foldr OldTerm.add_term_names
   223           (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
   224         val (Ts, dT) = split_last ((uncurry take) (i+1, fst (strip_type T)));
   225 
   226         fun pcase [] [] [] gr = ([], gr)
   227           | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
   228               let
   229                 val j = length cargs;
   230                 val xs = Name.variant_list names (replicate j "x");
   231                 val Us' = (uncurry take) (j, fst (strip_type U));
   232                 val frees = map Free (xs ~~ Us');
   233                 val (cp, gr0) = invoke_codegen thy defs dep module false
   234                   (list_comb (Const (cname, Us' ---> dT), frees)) gr;
   235                 val t' = Envir.beta_norm (list_comb (t, frees));
   236                 val (p, gr1) = invoke_codegen thy defs dep module false t' gr0;
   237                 val (ps, gr2) = pcase cs ts Us gr1;
   238               in
   239                 ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
   240               end;
   241 
   242         val (ps1, gr1) = pcase constrs ts1 Ts gr ;
   243         val ps = flat (separate [Pretty.brk 1, str "| "] ps1);
   244         val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
   245         val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
   246       in ((if not (null ts2) andalso brack then parens else I)
   247         (Pretty.block (separate (Pretty.brk 1)
   248           (Pretty.block ([str "(case ", p, str " of",
   249              Pretty.brk 1] @ ps @ [str ")"]) :: ps2))), gr3)
   250       end
   251   end;
   252 
   253 
   254 (* constructors *)
   255 
   256 fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
   257   let val i = length args
   258   in if i > 1 andalso length ts < i then
   259       invoke_codegen thy defs dep module brack (eta_expand c ts i) gr
   260      else
   261        let
   262          val id = mk_qual_id module (get_const_id gr s);
   263          val (ps, gr') = fold_map
   264            (invoke_codegen thy defs dep module (i = 1)) ts gr;
   265        in (case args of
   266           _ :: _ :: _ => (if brack then parens else I)
   267             (Pretty.block [str id, Pretty.brk 1, mk_tuple ps])
   268         | _ => (mk_app brack (str id) ps), gr')
   269        end
   270   end;
   271 
   272 
   273 (* code generators for terms and types *)
   274 
   275 fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
   276    (c as Const (s, T), ts) =>
   277      (case Datatype.info_of_case thy s of
   278         SOME {index, descr, ...} =>
   279           if is_some (get_assoc_code thy (s, T)) then NONE else
   280           SOME (pretty_case thy defs dep module brack
   281             (#3 (the (AList.lookup op = descr index))) c ts gr )
   282       | NONE => case (Datatype.info_of_constr thy (s, T), strip_type T) of
   283         (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
   284           if is_some (get_assoc_code thy (s, T)) then NONE else
   285           let
   286             val SOME (tyname', _, constrs) = AList.lookup op = descr index;
   287             val SOME args = AList.lookup op = constrs s
   288           in
   289             if tyname <> tyname' then NONE
   290             else SOME (pretty_constr thy defs
   291               dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
   292           end
   293       | _ => NONE)
   294  | _ => NONE);
   295 
   296 fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   297       (case Datatype.get_info thy s of
   298          NONE => NONE
   299        | SOME {descr, sorts, ...} =>
   300            if is_some (get_assoc_type thy s) then NONE else
   301            let
   302              val (ps, gr') = fold_map
   303                (invoke_tycodegen thy defs dep module false) Ts gr;
   304              val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
   305              val (tyid, gr''') = mk_type_id module' s gr''
   306            in SOME (Pretty.block ((if null Ts then [] else
   307                [mk_tuple ps, str " "]) @
   308                [str (mk_qual_id module tyid)]), gr''')
   309            end)
   310   | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   311 
   312 
   313 (** generic code generator **)
   314 
   315 (* liberal addition of code data for datatypes *)
   316 
   317 fun mk_constr_consts thy vs dtco cos =
   318   let
   319     val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
   320     val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
   321   in if is_some (try (Code.constrset_of_consts thy) cs')
   322     then SOME cs
   323     else NONE
   324   end;
   325 
   326 
   327 (* case certificates *)
   328 
   329 fun mk_case_cert thy tyco =
   330   let
   331     val raw_thms =
   332       (#case_rewrites o Datatype.the_info thy) tyco;
   333     val thms as hd_thm :: _ = raw_thms
   334       |> Conjunction.intr_balanced
   335       |> Thm.unvarify
   336       |> Conjunction.elim_balanced (length raw_thms)
   337       |> map Simpdata.mk_meta_eq
   338       |> map Drule.zero_var_indexes
   339     val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
   340       | _ => I) (Thm.prop_of hd_thm) [];
   341     val rhs = hd_thm
   342       |> Thm.prop_of
   343       |> Logic.dest_equals
   344       |> fst
   345       |> Term.strip_comb
   346       |> apsnd (fst o split_last)
   347       |> list_comb;
   348     val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
   349     val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   350   in
   351     thms
   352     |> Conjunction.intr_balanced
   353     |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
   354     |> Thm.implies_intr asm
   355     |> Thm.generalize ([], params) 0
   356     |> AxClass.unoverload thy
   357     |> Thm.varifyT
   358   end;
   359 
   360 
   361 (* equality *)
   362 
   363 fun mk_eq_eqns thy dtco =
   364   let
   365     val (vs, cos) = Datatype.the_spec thy dtco;
   366     val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
   367       Datatype.the_info thy dtco;
   368     val ty = Type (dtco, map TFree vs);
   369     fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
   370       $ t1 $ t2;
   371     fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
   372     fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
   373     val triv_injects = map_filter
   374      (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
   375        | _ => NONE) cos;
   376     fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
   377       trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
   378     val injects = map prep_inject (nth (DatatypeProp.make_injs [descr] vs) index);
   379     fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
   380       [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
   381     val distincts = maps prep_distinct (snd (nth (DatatypeProp.make_distincts [descr] vs) index));
   382     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
   383     val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
   384       (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
   385     fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
   386       |> Simpdata.mk_eq;
   387   in (map prove (triv_injects @ injects @ distincts), prove refl) end;
   388 
   389 fun add_equality vs dtcos thy =
   390   let
   391     fun add_def dtco lthy =
   392       let
   393         val ty = Type (dtco, map TFree vs);
   394         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
   395           $ Free ("x", ty) $ Free ("y", ty);
   396         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
   397           (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
   398         val def' = Syntax.check_term lthy def;
   399         val ((_, (_, thm)), lthy') = Specification.definition
   400           (NONE, (Attrib.empty_binding, def')) lthy;
   401         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   402         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   403       in (thm', lthy') end;
   404     fun tac thms = Class.intro_classes_tac []
   405       THEN ALLGOALS (ProofContext.fact_tac thms);
   406     fun add_eq_thms dtco =
   407       Theory.checkpoint
   408       #> `(fn thy => mk_eq_eqns thy dtco)
   409       #-> (fn (thms, thm) =>
   410         Code.add_nbe_eqn thm
   411         #> fold_rev Code.add_eqn thms);
   412   in
   413     thy
   414     |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
   415     |> fold_map add_def dtcos
   416     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
   417          (fn _ => fn def_thms => tac def_thms) def_thms)
   418     |-> (fn def_thms => fold Code.del_eqn def_thms)
   419     |> fold add_eq_thms dtcos
   420   end;
   421 
   422 
   423 (* register a datatype etc. *)
   424 
   425 fun add_all_code config dtcos thy =
   426   let
   427     val (vs :: _, coss) = (split_list o map (Datatype.the_spec thy)) dtcos;
   428     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
   429     val css = if exists is_none any_css then []
   430       else map_filter I any_css;
   431     val case_rewrites = maps (#case_rewrites o Datatype.the_info thy) dtcos;
   432     val certs = map (mk_case_cert thy) dtcos;
   433   in
   434     if null css then thy
   435     else thy
   436       |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
   437       |> fold Code.add_datatype css
   438       |> fold_rev Code.add_default_eqn case_rewrites
   439       |> fold Code.add_case certs
   440       |> add_equality vs dtcos
   441    end;
   442 
   443 
   444 (** theory setup **)
   445 
   446 val setup = 
   447   add_codegen "datatype" datatype_codegen
   448   #> add_tycodegen "datatype" datatype_tycodegen
   449   #> Datatype.interpretation add_all_code
   450 
   451 end;