src/HOL/Tools/primrec_package.ML
author haftmann
Tue May 26 17:29:34 2009 +0200 (2009-05-26)
changeset 31262 580510315dda
parent 31177 c39994cb152a
child 31269 dcbe1f9fe2cd
permissions -rw-r--r--
add_primrec_simple
     1 (*  Title:      HOL/Tools/primrec_package.ML
     2     Author:     Stefan Berghofer, TU Muenchen; Norbert Voelker, FernUni Hagen;
     3                 Florian Haftmann, TU Muenchen
     4 
     5 Package for defining functions on datatypes by primitive recursion.
     6 *)
     7 
     8 signature PRIMREC_PACKAGE =
     9 sig
    10   val add_primrec: (binding * typ option * mixfix) list ->
    11     (Attrib.binding * term) list -> local_theory -> thm list * local_theory
    12   val add_primrec_cmd: (binding * string option * mixfix) list ->
    13     (Attrib.binding * string) list -> local_theory -> thm list * local_theory
    14   val add_primrec_global: (binding * typ option * mixfix) list ->
    15     (Attrib.binding * term) list -> theory -> thm list * theory
    16   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
    17     (binding * typ option * mixfix) list ->
    18     (Attrib.binding * term) list -> theory -> thm list * theory
    19   val add_primrec_simple: ((binding * typ) * mixfix) list -> (binding * term) list ->
    20     local_theory -> (string * thm list list) * local_theory
    21 end;
    22 
    23 structure PrimrecPackage : PRIMREC_PACKAGE =
    24 struct
    25 
    26 open DatatypeAux;
    27 
    28 exception PrimrecError of string * term option;
    29 
    30 fun primrec_error msg = raise PrimrecError (msg, NONE);
    31 fun primrec_error_eqn msg eqn = raise PrimrecError (msg, SOME eqn);
    32 
    33 fun message s = if ! Toplevel.debug then tracing s else ();
    34 
    35 
    36 (* preprocessing of equations *)
    37 
    38 fun process_eqn is_fixed spec rec_fns =
    39   let
    40     val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
    41     val body = strip_qnt_body "all" spec;
    42     val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
    43       (fn Free (v, _) => insert (op =) v | _ => I) body []));
    44     val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
    45     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)
    46       handle TERM _ => primrec_error "not a proper equation";
    47     val (recfun, args) = strip_comb lhs;
    48     val fname = case recfun of Free (v, _) => if is_fixed v then v
    49           else primrec_error "illegal head of function equation"
    50       | _ => primrec_error "illegal head of function equation";
    51 
    52     val (ls', rest)  = take_prefix is_Free args;
    53     val (middle, rs') = take_suffix is_Free rest;
    54     val rpos = length ls';
    55 
    56     val (constr, cargs') = if null middle then primrec_error "constructor missing"
    57       else strip_comb (hd middle);
    58     val (cname, T) = dest_Const constr
    59       handle TERM _ => primrec_error "ill-formed constructor";
    60     val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
    61       primrec_error "cannot determine datatype associated with function"
    62 
    63     val (ls, cargs, rs) =
    64       (map dest_Free ls', map dest_Free cargs', map dest_Free rs')
    65       handle TERM _ => primrec_error "illegal argument in pattern";
    66     val lfrees = ls @ rs @ cargs;
    67 
    68     fun check_vars _ [] = ()
    69       | check_vars s vars = primrec_error (s ^ commas_quote (map fst vars)) eqn;
    70   in
    71     if length middle > 1 then
    72       primrec_error "more than one non-variable in pattern"
    73     else
    74      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    75       check_vars "extra variables on rhs: "
    76         (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
    77           |> filter_out (is_fixed o fst));
    78       case AList.lookup (op =) rec_fns fname of
    79         NONE =>
    80           (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eqn))]))::rec_fns
    81       | SOME (_, rpos', eqns) =>
    82           if AList.defined (op =) eqns cname then
    83             primrec_error "constructor already occurred as pattern"
    84           else if rpos <> rpos' then
    85             primrec_error "position of recursive argument inconsistent"
    86           else
    87             AList.update (op =)
    88               (fname, (tname, rpos, (cname, (ls, cargs, rs, rhs, eqn))::eqns))
    89               rec_fns)
    90   end handle PrimrecError (msg, NONE) => primrec_error_eqn msg spec;
    91 
    92 fun process_fun descr eqns (i, fname) (fnames, fnss) =
    93   let
    94     val (_, (tname, _, constrs)) = nth descr i;
    95 
    96     (* substitute "fname ls x rs" by "y ls rs" for (x, (_, y)) in subs *)
    97 
    98     fun subst [] t fs = (t, fs)
    99       | subst subs (Abs (a, T, t)) fs =
   100           fs
   101           |> subst subs t
   102           |-> (fn t' => pair (Abs (a, T, t')))
   103       | subst subs (t as (_ $ _)) fs =
   104           let
   105             val (f, ts) = strip_comb t;
   106           in
   107             if is_Free f
   108               andalso member (fn ((v, _), (w, _)) => v = w) eqns (dest_Free f) then
   109               let
   110                 val (fname', _) = dest_Free f;
   111                 val (_, rpos, _) = the (AList.lookup (op =) eqns fname');
   112                 val (ls, rs) = chop rpos ts
   113                 val (x', rs') = case rs
   114                  of x' :: rs => (x', rs)
   115                   | [] => primrec_error ("not enough arguments in recursive application\n"
   116                       ^ "of function " ^ quote fname' ^ " on rhs");
   117                 val (x, xs) = strip_comb x';
   118               in case AList.lookup (op =) subs x
   119                of NONE =>
   120                     fs
   121                     |> fold_map (subst subs) ts
   122                     |-> (fn ts' => pair (list_comb (f, ts')))
   123                 | SOME (i', y) =>
   124                     fs
   125                     |> fold_map (subst subs) (xs @ ls @ rs')
   126                     ||> process_fun descr eqns (i', fname')
   127                     |-> (fn ts' => pair (list_comb (y, ts')))
   128               end
   129             else
   130               fs
   131               |> fold_map (subst subs) (f :: ts)
   132               |-> (fn (f'::ts') => pair (list_comb (f', ts')))
   133           end
   134       | subst _ t fs = (t, fs);
   135 
   136     (* translate rec equations into function arguments suitable for rec comb *)
   137 
   138     fun trans eqns (cname, cargs) (fnames', fnss', fns) =
   139       (case AList.lookup (op =) eqns cname of
   140           NONE => (warning ("No equation for constructor " ^ quote cname ^
   141             "\nin definition of function " ^ quote fname);
   142               (fnames', fnss', (Const ("HOL.undefined", dummyT))::fns))
   143         | SOME (ls, cargs', rs, rhs, eq) =>
   144             let
   145               val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
   146               val rargs = map fst recs;
   147               val subs = map (rpair dummyT o fst)
   148                 (rev (Term.rename_wrt_term rhs rargs));
   149               val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
   150                 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
   151                   handle PrimrecError (s, NONE) => primrec_error_eqn s eq
   152             in (fnames'', fnss'',
   153                 (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
   154             end)
   155 
   156   in (case AList.lookup (op =) fnames i of
   157       NONE =>
   158         if exists (fn (_, v) => fname = v) fnames then
   159           primrec_error ("inconsistent functions for datatype " ^ quote tname)
   160         else
   161           let
   162             val (_, _, eqns) = the (AList.lookup (op =) eqns fname);
   163             val (fnames', fnss', fns) = fold_rev (trans eqns) constrs
   164               ((i, fname)::fnames, fnss, [])
   165           in
   166             (fnames', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
   167           end
   168     | SOME fname' =>
   169         if fname = fname' then (fnames, fnss)
   170         else primrec_error ("inconsistent functions for datatype " ^ quote tname))
   171   end;
   172 
   173 
   174 (* prepare functions needed for definitions *)
   175 
   176 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
   177   case AList.lookup (op =) fns i of
   178      NONE =>
   179        let
   180          val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
   181            replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
   182              dummyT ---> HOLogic.unitT)) constrs;
   183          val _ = warning ("No function definition for datatype " ^ quote tname)
   184        in
   185          (dummy_fns @ fs, defs)
   186        end
   187    | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname) :: defs);
   188 
   189 
   190 (* make definition *)
   191 
   192 fun make_def ctxt fixes fs (fname, ls, rec_name, tname) =
   193   let
   194     val SOME (var, varT) = get_first (fn ((b, T), mx) =>
   195       if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes;
   196     val def_name = Thm.def_name (Long_Name.base_name fname);
   197     val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
   198       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
   199     val rhs = singleton (Syntax.check_terms ctxt)
   200       (TypeInfer.constrain varT raw_rhs);
   201   in (var, ((Binding.name def_name, []), rhs)) end;
   202 
   203 
   204 (* find datatypes which contain all datatypes in tnames' *)
   205 
   206 fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
   207   | find_dts dt_info tnames' (tname::tnames) =
   208       (case Symtab.lookup dt_info tname of
   209           NONE => primrec_error (quote tname ^ " is not a datatype")
   210         | SOME dt =>
   211             if tnames' subset (map (#1 o snd) (#descr dt)) then
   212               (tname, dt)::(find_dts dt_info tnames' tnames)
   213             else find_dts dt_info tnames' tnames);
   214 
   215 
   216 (* distill primitive definition(s) from primrec specification *)
   217 
   218 fun distill lthy fixes eqs = 
   219   let
   220     val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
   221       orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
   222     val tnames = distinct (op =) (map (#1 o snd) eqns);
   223     val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
   224     val main_fns = map (fn (tname, {index, ...}) =>
   225       (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
   226     val {descr, rec_names, rec_rewrites, ...} =
   227       if null dts then primrec_error
   228         ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
   229       else snd (hd dts);
   230     val (fnames, fnss) = fold_rev (process_fun descr eqns) main_fns ([], []);
   231     val (fs, raw_defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
   232     val defs = map (make_def lthy fixes fs) raw_defs;
   233     val names = map snd fnames;
   234     val names_eqns = map fst eqns;
   235     val _ = if gen_eq_set (op =) (names, names_eqns) then ()
   236       else primrec_error ("functions " ^ commas_quote names_eqns ^
   237         "\nare not mutually recursive");
   238     val rec_rewrites' = map mk_meta_eq rec_rewrites;
   239     val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
   240     fun prove lthy defs =
   241       let
   242         val rewrites = rec_rewrites' @ map (snd o snd) defs;
   243         fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
   244         val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
   245       in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
   246   in ((prefix, (fs, defs)), prove) end
   247   handle PrimrecError (msg, some_eqn) =>
   248     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
   249      of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
   250       | NONE => ""));
   251 
   252 
   253 (* primrec definition *)
   254 
   255 fun add_primrec_simple fixes spec lthy =
   256   let
   257     val ((prefix, (fs, defs)), prove) = distill lthy fixes (map snd spec);
   258   in
   259     lthy
   260     |> fold_map (LocalTheory.define Thm.definitionK) defs
   261     |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   262   end;
   263 
   264 local
   265 
   266 fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
   267   let
   268     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
   269     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
   270       (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
   271     fun simp_attr_binding prefix = (Binding.qualify false prefix (Binding.name "simps"),
   272       map (Attrib.internal o K)
   273         [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
   274   in
   275     lthy
   276     |> set_group ? LocalTheory.set_group (serial_string ())
   277     |> add_primrec_simple fixes spec
   278     |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
   279           (attr_bindings prefix ~~ simps)
   280     #-> (fn simps' => LocalTheory.note Thm.generatedK
   281           (simp_attr_binding prefix, maps snd simps')))
   282     |>> snd
   283   end;
   284 
   285 in
   286 
   287 val add_primrec = gen_primrec false Specification.check_spec;
   288 val add_primrec_cmd = gen_primrec true Specification.read_spec;
   289 
   290 end;
   291 
   292 fun add_primrec_global fixes specs thy =
   293   let
   294     val lthy = TheoryTarget.init NONE thy;
   295     val (simps, lthy') = add_primrec fixes specs lthy;
   296     val simps' = ProofContext.export lthy' lthy simps;
   297   in (simps', LocalTheory.exit_global lthy') end;
   298 
   299 fun add_primrec_overloaded ops fixes specs thy =
   300   let
   301     val lthy = TheoryTarget.overloading ops thy;
   302     val (simps, lthy') = add_primrec fixes specs lthy;
   303     val simps' = ProofContext.export lthy' lthy simps;
   304   in (simps', LocalTheory.exit_global lthy') end;
   305 
   306 
   307 (* outer syntax *)
   308 
   309 local structure P = OuterParse and K = OuterKeyword in
   310 
   311 val opt_unchecked_name =
   312   Scan.optional (P.$$$ "(" |-- P.!!!
   313     (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
   314       P.name >> pair false) --| P.$$$ ")")) (false, "");
   315 
   316 val old_primrec_decl =
   317   opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
   318 
   319 val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
   320 
   321 val _ =
   322   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   323     ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
   324       Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
   325     || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
   326       Toplevel.theory (snd o
   327         (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec)
   328           alt_name (map P.triple_swap eqns)))));
   329 
   330 end;
   331 
   332 end;