src/Pure/Tools/codegen_func.ML
changeset 22484 25dfebd7b4c8
parent 22475 bd3378255cc8
child 22554 d1499fff65d8
     1.1 --- a/src/Pure/Tools/codegen_func.ML	Tue Mar 20 15:52:40 2007 +0100
     1.2 +++ b/src/Pure/Tools/codegen_func.ML	Tue Mar 20 15:52:41 2007 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val assert_rew: thm -> thm
     1.6    val mk_rew: thm -> thm list
     1.7 -  val assert_func: thm -> thm
     1.8 -  val mk_func: thm -> (CodegenConsts.const * thm) list
     1.9 +  val assert_func: bool -> thm -> thm option
    1.10 +  val mk_func: bool -> thm -> (CodegenConsts.const * thm) list
    1.11    val mk_head: thm -> CodegenConsts.const * thm
    1.12    val dest_func: thm -> (string * typ) * term list
    1.13    val typ_func: thm -> typ
    1.14 @@ -77,8 +77,18 @@
    1.15  val mk_head = lift_thm_thy (fn thy => fn thm =>
    1.16    ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
    1.17  
    1.18 -fun assert_func thm = case try dest_func thm
    1.19 - of SOME (c_ty as (c, ty), args) =>
    1.20 +local
    1.21 +
    1.22 +exception BAD of string;
    1.23 +
    1.24 +fun handle_bad strict thm msg =
    1.25 +  if strict then error (msg ^ ": " ^ string_of_thm thm)
    1.26 +    else (warning (msg ^ ": " ^ string_of_thm thm); NONE);
    1.27 +
    1.28 +in
    1.29 +
    1.30 +fun assert_func strict thm = case try dest_func thm
    1.31 + of SOME (c_ty as (c, ty), args) => (
    1.32        let
    1.33          val thy = Thm.theory_of_thm thm;
    1.34          val _ =
    1.35 @@ -86,23 +96,25 @@
    1.36              ((fold o fold_aterms) (fn Var (v, _) => cons v
    1.37                | _ => I
    1.38              ) args [])
    1.39 -          then bad_thm "Repeated variables on left hand side of defining equation" thm
    1.40 +          then raise BAD "Repeated variables on left hand side of defining equation"
    1.41            else ()
    1.42 -        fun check _ (Abs _) = bad_thm
    1.43 -              "Abstraction on left hand side of defining equation" thm
    1.44 +        fun check _ (Abs _) = raise BAD
    1.45 +              "Abstraction on left hand side of defining equation"
    1.46            | check 0 (Var _) = ()
    1.47 -          | check _ (Var _) = bad_thm
    1.48 -              "Variable with application on left hand side of defining equation" thm
    1.49 +          | check _ (Var _) = raise BAD
    1.50 +              "Variable with application on left hand side of defining equation"
    1.51            | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
    1.52            | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
    1.53 -              then bad_thm
    1.54 -                ("Partially applied constant on left hand side of defining equation") thm
    1.55 +              then raise BAD
    1.56 +                ("Partially applied constant on left hand side of defining equation")
    1.57                else ();
    1.58          val _ = map (check 0) args;
    1.59 -      in thm end
    1.60 -  | NONE => bad_thm "Not a defining equation" thm;
    1.61 +      in SOME thm end handle BAD msg => handle_bad strict thm msg)
    1.62 +  | NONE => handle_bad strict thm "Not a defining equation";
    1.63  
    1.64 -val mk_func = map (mk_head o assert_func) o mk_rew;
    1.65 +end;
    1.66 +
    1.67 +fun mk_func strict = map_filter (Option.map mk_head o assert_func strict) o mk_rew;
    1.68  
    1.69  
    1.70  (* utilities *)