clarified matter of "proper" flag in code equations
authorhaftmann
Mon May 11 10:53:19 2009 +0200 (2009-05-11)
changeset 310903be41b271023
parent 31089 11001968caae
child 31091 8316d22f10f5
clarified matter of "proper" flag in code equations
src/HOL/Library/Efficient_Nat.thy
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon May 11 09:40:39 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon May 11 10:53:19 2009 +0200
     1.3 @@ -179,10 +179,8 @@
     1.4         else NONE
     1.5    end;
     1.6  
     1.7 -fun eqn_suc_preproc thy = map fst
     1.8 -  #> gen_eqn_suc_preproc
     1.9 -      @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
    1.10 -  #> (Option.map o map) (Code_Unit.mk_eqn thy);
    1.11 +val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
    1.12 +  @{thm Suc_if_eq} I (fst o Logic.dest_equals));
    1.13  
    1.14  fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
    1.15    @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon May 11 09:40:39 2009 +0200
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 11 10:53:19 2009 +0200
     2.3 @@ -25,13 +25,13 @@
     2.4  
     2.5  fun add_thm NONE thm thy = Code.add_eqn thm thy
     2.6    | add_thm (SOME module_name) thm thy =
     2.7 -      case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
     2.8 -       of SOME (thm', _) => let val c = Code_Unit.const_eqn thy thm'
     2.9 -            in thy
    2.10 -              |> ModuleData.map (Symtab.update (c, module_name))
    2.11 -              |> Code.add_eqn thm'
    2.12 -            end
    2.13 -        | NONE => Code.add_eqn thm thy;
    2.14 +      let
    2.15 +        val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true)
    2.16 +      in
    2.17 +        thy
    2.18 +        |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name))
    2.19 +        |> Code.add_eqn thm'
    2.20 +      end;
    2.21  
    2.22  fun meta_eq_to_obj_eq thy thm =
    2.23    let
     3.1 --- a/src/HOL/Tools/typecopy_package.ML	Mon May 11 09:40:39 2009 +0200
     3.2 +++ b/src/HOL/Tools/typecopy_package.ML	Mon May 11 10:53:19 2009 +0200
     3.3 @@ -150,7 +150,7 @@
     3.4                  THEN ALLGOALS (rtac @{thm refl})) def_thm)
     3.5      |-> (fn def_thm => Code.add_eqn def_thm)
     3.6      |> `(fn thy => mk_eq_refl thy)
     3.7 -    |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm)
     3.8 +    |-> (fn refl_thm => Code.add_nbe_eqn refl_thm)
     3.9    end;
    3.10  
    3.11  val setup =
     4.1 --- a/src/Pure/Isar/code.ML	Mon May 11 09:40:39 2009 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Mon May 11 10:53:19 2009 +0200
     4.3 @@ -20,6 +20,8 @@
     4.4    val add_inline: thm -> theory -> theory
     4.5    val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
     4.6    val del_functrans: string -> theory -> theory
     4.7 +  val simple_functrans: (theory -> thm list -> thm list option)
     4.8 +    -> theory -> (thm * bool) list -> (thm * bool) list option
     4.9    val add_datatype: (string * typ) list -> theory -> theory
    4.10    val add_datatype_cmd: string list -> theory -> theory
    4.11    val type_interpretation:
    4.12 @@ -456,16 +458,6 @@
    4.13            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
    4.14        in map (Thm.instantiate (instT, [])) thms' end;
    4.15  
    4.16 -fun check_proper (eqn as (thm, proper)) =
    4.17 -  if proper then eqn else Code_Unit.bad_thm
    4.18 -    ("Duplicate variables on left hand side of code equation:\n"
    4.19 -      ^ Display.string_of_thm thm);
    4.20 -
    4.21 -fun mk_eqn thy proper =
    4.22 -  Code_Unit.error_thm ((if proper then check_proper else I) o Code_Unit.mk_eqn thy);
    4.23 -fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy);
    4.24 -fun mk_default_eqn thy = Code_Unit.try_thm (check_proper o Code_Unit.mk_eqn thy);
    4.25 -
    4.26  
    4.27  (** interfaces and attributes **)
    4.28  
    4.29 @@ -489,50 +481,44 @@
    4.30  
    4.31  fun is_constr thy = is_some o get_datatype_of_constr thy;
    4.32  
    4.33 -fun recheck_eqn thy = Code_Unit.error_thm
    4.34 -  (Code_Unit.assert_linear (is_constr thy) o apfst (Code_Unit.assert_eqn thy));
    4.35 +fun assert_eqn thy = Code_Unit.assert_eqn thy (is_constr thy);
    4.36  
    4.37 -fun recheck_eqns_const thy c eqns =
    4.38 +fun assert_eqns_const thy c eqns =
    4.39    let
    4.40      fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm
    4.41        then eqn else error ("Wrong head of code equation,\nexpected constant "
    4.42          ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
    4.43 -  in map (cert o recheck_eqn thy) eqns end;
    4.44 +  in map (cert o assert_eqn thy) eqns end;
    4.45  
    4.46  fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
    4.47    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
    4.48      o apfst) (fn (_, eqns) => (true, f eqns));
    4.49  
    4.50 -fun gen_add_eqn proper default thm thy =
    4.51 -  case (if default then mk_default_eqn thy else SOME o mk_eqn thy proper) thm
    4.52 -   of SOME (thm, _) =>
    4.53 -        let
    4.54 -          val c = Code_Unit.const_eqn thy thm;
    4.55 -          val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
    4.56 -            then error ("Rejected polymorphic code equation for overloaded constant:\n"
    4.57 -              ^ Display.string_of_thm thm)
    4.58 -            else ();
    4.59 -          val _ = if not default andalso is_constr thy c
    4.60 -            then error ("Rejected code equation for datatype constructor:\n"
    4.61 -              ^ Display.string_of_thm thm)
    4.62 -            else ();
    4.63 -        in change_eqns false c (add_thm thy default (thm, proper)) thy end
    4.64 +fun gen_add_eqn default (eqn as (thm, _)) thy =
    4.65 +  let val c = Code_Unit.const_eqn thy thm
    4.66 +  in change_eqns false c (add_thm thy default eqn) thy end;
    4.67 +
    4.68 +fun add_eqn thm thy =
    4.69 +  gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, true)) thy;
    4.70 +
    4.71 +fun add_default_eqn thm thy =
    4.72 +  case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
    4.73 +   of SOME eqn => gen_add_eqn true eqn thy
    4.74      | NONE => thy;
    4.75  
    4.76 -val add_eqn = gen_add_eqn true false;
    4.77 -val add_default_eqn = gen_add_eqn true true;
    4.78 -val add_nbe_eqn = gen_add_eqn false false;
    4.79 +fun add_nbe_eqn thm thy =
    4.80 +  gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, false)) thy;
    4.81  
    4.82  fun add_eqnl (c, lthms) thy =
    4.83    let
    4.84 -    val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms;
    4.85 +    val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms;
    4.86    in change_eqns false c (add_lthms lthms') thy end;
    4.87  
    4.88  val add_default_eqn_attribute = Thm.declaration_attribute
    4.89    (fn thm => Context.mapping (add_default_eqn thm) I);
    4.90  val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
    4.91  
    4.92 -fun del_eqn thm thy = case mk_syntactic_eqn thy thm
    4.93 +fun del_eqn thm thy = case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
    4.94   of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy
    4.95    | NONE => thy;
    4.96  
    4.97 @@ -598,6 +584,10 @@
    4.98    (map_exec_purge NONE o map_thmproc o apsnd)
    4.99      (delete_force "function transformer" name);
   4.100  
   4.101 +fun simple_functrans f thy eqns = case f thy (map fst eqns)
   4.102 + of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
   4.103 +  | NONE => NONE;
   4.104 +
   4.105  val _ = Context.>> (Context.map_theory
   4.106    (let
   4.107      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   4.108 @@ -623,7 +613,7 @@
   4.109    | apply_functrans thy c [] eqns = eqns
   4.110    | apply_functrans thy c functrans eqns = eqns
   4.111        |> perhaps (perhaps_loop (perhaps_apply functrans))
   4.112 -      |> recheck_eqns_const thy c;
   4.113 +      |> assert_eqns_const thy c;
   4.114  
   4.115  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   4.116  
   4.117 @@ -644,7 +634,7 @@
   4.118      |> apply_functrans thy c functrans
   4.119      |> (map o apfst) (Code_Unit.rewrite_eqn pre)
   4.120      |> (map o apfst) (AxClass.unoverload thy)
   4.121 -    |> map (recheck_eqn thy)
   4.122 +    |> map (assert_eqn thy)
   4.123      |> burrow_fst (common_typ_eqns thy)
   4.124    end;
   4.125  
     5.1 --- a/src/Pure/Isar/code_unit.ML	Mon May 11 09:40:39 2009 +0200
     5.2 +++ b/src/Pure/Isar/code_unit.ML	Mon May 11 10:53:19 2009 +0200
     5.3 @@ -6,12 +6,6 @@
     5.4  
     5.5  signature CODE_UNIT =
     5.6  sig
     5.7 -  (*generic non-sense*)
     5.8 -  val bad_thm: string -> 'a
     5.9 -  val error_thm: ('a -> 'b) -> 'a -> 'b
    5.10 -  val warning_thm: ('a -> 'b) -> 'a -> 'b option
    5.11 -  val try_thm: ('a -> 'b) -> 'a -> 'b option
    5.12 -
    5.13    (*typ instantiations*)
    5.14    val typscheme: theory -> string * typ -> (string * sort) list * typ
    5.15    val inst_thm: theory -> sort Vartab.table -> thm -> thm
    5.16 @@ -35,11 +29,11 @@
    5.17      -> string * ((string * sort) list * (string * typ list) list)
    5.18  
    5.19    (*code equations*)
    5.20 -  val assert_eqn: theory -> thm -> thm
    5.21 -  val mk_eqn: theory -> thm -> thm * bool
    5.22 -  val assert_linear: (string -> bool) -> thm * bool -> thm * bool
    5.23 +  val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
    5.24 +  val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
    5.25 +  val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
    5.26    val const_eqn: theory -> thm -> string
    5.27 -  val const_typ_eqn: thm -> string * typ
    5.28 +    val const_typ_eqn: thm -> string * typ
    5.29    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
    5.30    val expand_eta: theory -> int -> thm -> thm
    5.31    val rewrite_eqn: simpset -> thm -> thm
    5.32 @@ -57,13 +51,6 @@
    5.33  
    5.34  (* auxiliary *)
    5.35  
    5.36 -exception BAD_THM of string;
    5.37 -fun bad_thm msg = raise BAD_THM msg;
    5.38 -fun error_thm f thm = f thm handle BAD_THM msg => error msg;
    5.39 -fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
    5.40 -  => (warning ("code generator: " ^ msg); NONE);
    5.41 -fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
    5.42 -
    5.43  fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
    5.44  fun string_of_const thy c = case AxClass.inst_of_param thy c
    5.45   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    5.46 @@ -323,39 +310,50 @@
    5.47  
    5.48  (* code equations *)
    5.49  
    5.50 -fun assert_eqn thy thm =
    5.51 +exception BAD_THM of string;
    5.52 +fun bad_thm msg = raise BAD_THM msg;
    5.53 +fun error_thm f thm = f thm handle BAD_THM msg => error msg;
    5.54 +fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
    5.55 +
    5.56 +fun is_linear thm =
    5.57 +  let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
    5.58 +  in not (has_duplicates (op =) ((fold o fold_aterms)
    5.59 +    (fn Var (v, _) => cons v | _ => I) args [])) end;
    5.60 +
    5.61 +fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) =
    5.62    let
    5.63      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
    5.64        handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
    5.65 -          | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
    5.66 +           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
    5.67      fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
    5.68 -      | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
    5.69 +      | Free _ => bad_thm ("Illegal free variable in equation\n"
    5.70            ^ Display.string_of_thm thm)
    5.71        | _ => I) t [];
    5.72      fun tvars_of t = fold_term_types (fn _ =>
    5.73        fold_atyps (fn TVar (v, _) => insert (op =) v
    5.74          | TFree _ => bad_thm 
    5.75 -      ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
    5.76 +      ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
    5.77      val lhs_vs = vars_of lhs;
    5.78      val rhs_vs = vars_of rhs;
    5.79      val lhs_tvs = tvars_of lhs;
    5.80      val rhs_tvs = tvars_of rhs;
    5.81      val _ = if null (subtract (op =) lhs_vs rhs_vs)
    5.82        then ()
    5.83 -      else bad_thm ("Free variables on right hand side of rewrite theorem\n"
    5.84 +      else bad_thm ("Free variables on right hand side of equation\n"
    5.85          ^ Display.string_of_thm thm);
    5.86      val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
    5.87        then ()
    5.88 -      else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
    5.89 +      else bad_thm ("Free type variables on right hand side of equation\n"
    5.90          ^ Display.string_of_thm thm)    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
    5.91 -    val (c, ty) = case head of Const c_ty => c_ty | _ =>
    5.92 -      bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
    5.93 +    val (c, ty) = case head
    5.94 +     of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
    5.95 +      | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
    5.96      fun check _ (Abs _) = bad_thm
    5.97            ("Abstraction on left hand side of equation\n"
    5.98              ^ Display.string_of_thm thm)
    5.99        | check 0 (Var _) = ()
   5.100        | check _ (Var _) = bad_thm
   5.101 -          ("Variable with application on left hand side of code equation\n"
   5.102 +          ("Variable with application on left hand side of equation\n"
   5.103              ^ Display.string_of_thm thm)
   5.104        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   5.105        | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
   5.106 @@ -364,44 +362,44 @@
   5.107                 ^ Display.string_of_thm thm)
   5.108            else ();
   5.109      val _ = map (check 0) args;
   5.110 +    val _ = (map o map_aterms) (fn t as Const (c, _) => if is_constr_pat c then t
   5.111 +          else bad_thm (quote c ^ "is not a constructor, on left hand side of equation\n"
   5.112 +            ^ Display.string_of_thm thm)
   5.113 +      | t => t) args;
   5.114 +    val _ = if not proper orelse is_linear thm then ()
   5.115 +      else bad_thm ("Duplicate variables on left hand side of equation\n"
   5.116 +        ^ Display.string_of_thm thm);
   5.117 +    val _ = if (is_none o AxClass.class_of_param thy) c
   5.118 +      then ()
   5.119 +      else bad_thm ("Polymorphic constant as head in equation\n"
   5.120 +        ^ Display.string_of_thm thm)
   5.121 +    val _ = if not (is_constr_head c)
   5.122 +      then ()
   5.123 +      else bad_thm ("Constructor as head in equation\n"
   5.124 +        ^ Display.string_of_thm thm)
   5.125      val ty_decl = Sign.the_const_type thy c;
   5.126      val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   5.127        then () else bad_thm ("Type\n" ^ string_of_typ thy ty
   5.128 -           ^ "\nof code equation\n"
   5.129 +           ^ "\nof equation\n"
   5.130             ^ Display.string_of_thm thm
   5.131             ^ "\nis incompatible with declared function type\n"
   5.132             ^ string_of_typ thy ty_decl)
   5.133 -  in thm end;
   5.134 -
   5.135 -fun add_linear thm =
   5.136 -  let
   5.137 -    val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   5.138 -    val linear = not (has_duplicates (op =)
   5.139 -      ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
   5.140 -  in (thm, linear) end;
   5.141 +  in (thm, proper) end;
   5.142  
   5.143 -fun assert_pat is_cons thm =
   5.144 -  let
   5.145 -    val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   5.146 -    val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t
   5.147 -          else bad_thm ("Not a constructor on left hand side of equation: "
   5.148 -            ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm)
   5.149 -      | t => t) args;
   5.150 -  in thm end;
   5.151 -
   5.152 -fun assert_linear is_cons (thm, false) = (thm, false)
   5.153 -  | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm))
   5.154 -      then (thm, true)
   5.155 -      else bad_thm
   5.156 -        ("Duplicate variables on left hand side of code equation:\n"
   5.157 -          ^ Display.string_of_thm thm);
   5.158 +fun assert_eqn thy is_constr = gen_assert_eqn thy is_constr is_constr;
   5.159  
   5.160  val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   5.161  
   5.162  fun typscheme_eqn thy = typscheme thy o const_typ_eqn;
   5.163  
   5.164 -(*permissive wrt. to overloaded constants!*)
   5.165 -fun mk_eqn thy = add_linear o assert_eqn thy o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   5.166 +(*these are permissive wrt. to overloaded constants!*)
   5.167 +fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
   5.168 +  apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
   5.169 +
   5.170 +fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
   5.171 +  o try_thm (gen_assert_eqn thy is_constr_head (K true))
   5.172 +  o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   5.173 +
   5.174  fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn;
   5.175  
   5.176