src/HOL/Tools/primrec_package.ML
changeset 19688 877b763ded7e
parent 19636 50515882049e
child 20046 9c8909fc5865
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Sat May 20 23:36:56 2006 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat May 20 23:36:57 2006 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4    val quiet_mode: bool ref
     1.5    val add_primrec: string -> ((bstring * string) * Attrib.src list) list
     1.6      -> theory -> theory * thm list
     1.7 +  val add_primrec_unchecked: string -> ((bstring * string) * Attrib.src list) list
     1.8 +    -> theory -> theory * thm list
     1.9    val add_primrec_i: string -> ((bstring * term) * attribute list) list
    1.10      -> theory -> theory * thm list
    1.11    val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
    1.12 @@ -223,7 +225,7 @@
    1.13      |> RuleCases.save induction
    1.14    end;
    1.15  
    1.16 -fun gen_primrec unchecked alt_name eqns_atts thy =
    1.17 +fun gen_primrec_i unchecked alt_name eqns_atts thy =
    1.18    let
    1.19      val (eqns, atts) = split_list eqns_atts;
    1.20      val sg = Theory.sign_of thy;
    1.21 @@ -269,10 +271,7 @@
    1.22      (thy''', simps')
    1.23    end;
    1.24  
    1.25 -val add_primrec_i = gen_primrec false;
    1.26 -val add_primrec_unchecked_i = gen_primrec true;
    1.27 -
    1.28 -fun add_primrec alt_name eqns thy =
    1.29 +fun gen_primrec unchecked alt_name eqns thy =
    1.30    let
    1.31      val sign = Theory.sign_of thy;
    1.32      val ((names, strings), srcss) = apfst split_list (split_list eqns);
    1.33 @@ -283,22 +282,33 @@
    1.34        handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts;
    1.35      val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts
    1.36    in
    1.37 -    add_primrec_i alt_name (names ~~ eqn_ts' ~~ atts) thy
    1.38 +    gen_primrec_i unchecked alt_name (names ~~ eqn_ts' ~~ atts) thy
    1.39    end;
    1.40  
    1.41 +val add_primrec = gen_primrec false;
    1.42 +val add_primrec_unchecked = gen_primrec true;
    1.43 +val add_primrec_i = gen_primrec_i false;
    1.44 +val add_primrec_unchecked_i = gen_primrec_i true;
    1.45 +
    1.46  
    1.47  (* outer syntax *)
    1.48  
    1.49  local structure P = OuterParse and K = OuterKeyword in
    1.50  
    1.51 +val opt_unchecked_name =
    1.52 +  Scan.optional (P.$$$ "(" |-- P.!!!
    1.53 +    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
    1.54 +      P.name >> pair false) --| P.$$$ ")")) (false, "");
    1.55 +
    1.56  val primrec_decl =
    1.57 -  Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
    1.58 -    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
    1.59 +  opt_unchecked_name -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
    1.60  
    1.61  val primrecP =
    1.62    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
    1.63 -    (primrec_decl >> (fn (alt_name, eqns) =>
    1.64 -      Toplevel.theory (#1 o add_primrec alt_name (map P.triple_swap eqns))));
    1.65 +    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
    1.66 +      Toplevel.theory (#1 o
    1.67 +        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
    1.68 +          (map P.triple_swap eqns))));
    1.69  
    1.70  val _ = OuterSyntax.add_parsers [primrecP];
    1.71