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