src/HOL/Tools/primrec.ML
author wenzelm
Thu Nov 19 14:46:33 2009 +0100 (2009-11-19)
changeset 33766 c679f05600cd
parent 33755 6dc1b67f2127
child 33963 977b94b64905
permissions -rw-r--r--
adapted Local_Theory.define -- eliminated odd thm kind;
     1 (*  Title:      HOL/Tools/primrec.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 =
     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 -> term list ->
    20     local_theory -> (string * thm list list) * local_theory
    21 end;
    22 
    23 structure Primrec : PRIMREC =
    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 (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.conceal (Binding.name def_name), []), rhs)) end;
   202 
   203 
   204 (* find datatypes which contain all datatypes in tnames' *)
   205 
   206 fun find_dts (dt_info : 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 subset (op =) (tnames', 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 (Datatype.get_all (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 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 frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
   243           if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
   244         val rewrites = rec_rewrites' @ map (snd o snd) defs;
   245         fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
   246         val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
   247       in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
   248   in ((prefix, (fs, defs)), prove) end
   249   handle PrimrecError (msg, some_eqn) =>
   250     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
   251      of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
   252       | NONE => ""));
   253 
   254 
   255 (* primrec definition *)
   256 
   257 fun add_primrec_simple fixes ts lthy =
   258   let
   259     val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   260   in
   261     lthy
   262     |> fold_map Local_Theory.define defs
   263     |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   264   end;
   265 
   266 local
   267 
   268 fun gen_primrec prep_spec raw_fixes raw_spec lthy =
   269   let
   270     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
   271     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
   272       (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
   273     fun simp_attr_binding prefix =
   274       (Binding.qualify true prefix (Binding.name "simps"),
   275         map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   276   in
   277     lthy
   278     |> add_primrec_simple fixes (map snd spec)
   279     |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
   280       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
   281     |>> snd
   282   end;
   283 
   284 in
   285 
   286 val add_primrec = gen_primrec Specification.check_spec;
   287 val add_primrec_cmd = gen_primrec Specification.read_spec;
   288 
   289 end;
   290 
   291 fun add_primrec_global fixes specs thy =
   292   let
   293     val lthy = Theory_Target.init NONE thy;
   294     val (simps, lthy') = add_primrec fixes specs lthy;
   295     val simps' = ProofContext.export lthy' lthy simps;
   296   in (simps', Local_Theory.exit_global lthy') end;
   297 
   298 fun add_primrec_overloaded ops fixes specs thy =
   299   let
   300     val lthy = Theory_Target.overloading ops thy;
   301     val (simps, lthy') = add_primrec fixes specs lthy;
   302     val simps' = ProofContext.export lthy' lthy simps;
   303   in (simps', Local_Theory.exit_global lthy') end;
   304 
   305 
   306 (* outer syntax *)
   307 
   308 local structure P = OuterParse and K = OuterKeyword in
   309 
   310 val opt_unchecked_name =
   311   Scan.optional (P.$$$ "(" |-- P.!!!
   312     (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
   313       P.name >> pair false) --| P.$$$ ")")) (false, "");
   314 
   315 val old_primrec_decl =
   316   opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
   317 
   318 val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
   319 
   320 val _ =
   321   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   322     ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
   323       Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
   324     || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
   325       Toplevel.theory (snd o
   326         (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
   327           alt_name (map P.triple_swap eqns)))));
   328 
   329 end;
   330 
   331 end;