1.1 --- a/src/Pure/Isar/code.ML	Mon May 11 09:40:38 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon May 11 09:40:38 2009 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  signature CODE =
     1.5  sig
     1.6    val add_eqn: thm -> theory -> theory
     1.7 -  val add_nonlinear_eqn: thm -> theory -> theory
     1.8 +  val add_nbe_eqn: thm -> theory -> theory
     1.9    val add_default_eqn: thm -> theory -> theory
    1.10    val add_default_eqn_attribute: attribute
    1.11    val add_default_eqn_attrib: Attrib.src
    1.12 @@ -109,7 +109,7 @@
    1.13  (* code equations *)
    1.14  
    1.15  type eqns = bool * (thm * bool) list lazy;
    1.16 -  (*default flag, theorems with linear flag (perhaps lazy)*)
    1.17 +  (*default flag, theorems with proper flag (perhaps lazy)*)
    1.18  
    1.19  fun pretty_lthms ctxt r = case Lazy.peek r
    1.20   of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
    1.21 @@ -122,18 +122,18 @@
    1.22          val thy_ref = Theory.check_thy thy;
    1.23        in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
    1.24  
    1.25 -fun add_drop_redundant thy (thm, linear) thms =
    1.26 +fun add_drop_redundant thy (thm, proper) thms =
    1.27    let
    1.28      val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    1.29      val args = args_of thm;
    1.30      val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
    1.31      fun matches_args args' = length args <= length args' andalso
    1.32        Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
    1.33 -    fun drop (thm', linear') = if (linear orelse not linear')
    1.34 +    fun drop (thm', proper') = if (proper orelse not proper')
    1.35        andalso matches_args (args_of thm') then 
    1.36          (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
    1.37        else false;
    1.38 -  in (thm, linear) :: filter_out drop thms end;
    1.39 +  in (thm, proper) :: filter_out drop thms end;
    1.40  
    1.41  fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
    1.42    | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
    1.43 @@ -456,15 +456,15 @@
    1.44            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
    1.45        in map (Thm.instantiate (instT, [])) thms' end;
    1.46  
    1.47 -fun check_linear (eqn as (thm, linear)) =
    1.48 -  if linear then eqn else Code_Unit.bad_thm
    1.49 +fun check_proper (eqn as (thm, proper)) =
    1.50 +  if proper then eqn else Code_Unit.bad_thm
    1.51      ("Duplicate variables on left hand side of code equation:\n"
    1.52        ^ Display.string_of_thm thm);
    1.53  
    1.54 -fun mk_eqn thy linear =
    1.55 -  Code_Unit.error_thm ((if linear then check_linear else I) o Code_Unit.mk_eqn thy);
    1.56 +fun mk_eqn thy proper =
    1.57 +  Code_Unit.error_thm ((if proper then check_proper else I) o Code_Unit.mk_eqn thy);
    1.58  fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy);
    1.59 -fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy);
    1.60 +fun mk_default_eqn thy = Code_Unit.try_thm (check_proper o Code_Unit.mk_eqn thy);
    1.61  
    1.62  
    1.63  (** interfaces and attributes **)
    1.64 @@ -487,12 +487,14 @@
    1.65         then SOME tyco else NONE
    1.66      | _ => NONE;
    1.67  
    1.68 +fun is_constr thy = is_some o get_datatype_of_constr thy;
    1.69 +
    1.70  fun recheck_eqn thy = Code_Unit.error_thm
    1.71 -  (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
    1.72 +  (Code_Unit.assert_linear (is_constr thy) o apfst (Code_Unit.assert_eqn thy));
    1.73  
    1.74  fun recheck_eqns_const thy c eqns =
    1.75    let
    1.76 -    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
    1.77 +    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm
    1.78        then eqn else error ("Wrong head of code equation,\nexpected constant "
    1.79          ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
    1.80    in map (cert o recheck_eqn thy) eqns end;
    1.81 @@ -501,25 +503,25 @@
    1.82    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
    1.83      o apfst) (fn (_, eqns) => (true, f eqns));
    1.84  
    1.85 -fun gen_add_eqn linear default thm thy =
    1.86 -  case (if default then mk_default_eqn thy else SOME o mk_eqn thy linear) thm
    1.87 +fun gen_add_eqn proper default thm thy =
    1.88 +  case (if default then mk_default_eqn thy else SOME o mk_eqn thy proper) thm
    1.89     of SOME (thm, _) =>
    1.90          let
    1.91 -          val c = Code_Unit.const_eqn thm;
    1.92 +          val c = Code_Unit.const_eqn thy thm;
    1.93            val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
    1.94              then error ("Rejected polymorphic code equation for overloaded constant:\n"
    1.95                ^ Display.string_of_thm thm)
    1.96              else ();
    1.97 -          val _ = if not default andalso (is_some o get_datatype_of_constr thy) c
    1.98 +          val _ = if not default andalso is_constr thy c
    1.99              then error ("Rejected code equation for datatype constructor:\n"
   1.100                ^ Display.string_of_thm thm)
   1.101              else ();
   1.102 -        in change_eqns false c (add_thm thy default (thm, linear)) thy end
   1.103 +        in change_eqns false c (add_thm thy default (thm, proper)) thy end
   1.104      | NONE => thy;
   1.105  
   1.106  val add_eqn = gen_add_eqn true false;
   1.107  val add_default_eqn = gen_add_eqn true true;
   1.108 -val add_nonlinear_eqn = gen_add_eqn false false;
   1.109 +val add_nbe_eqn = gen_add_eqn false false;
   1.110  
   1.111  fun add_eqnl (c, lthms) thy =
   1.112    let
   1.113 @@ -531,7 +533,7 @@
   1.114  val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
   1.115  
   1.116  fun del_eqn thm thy = case mk_syntactic_eqn thy thm
   1.117 - of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thm) (del_thm thm) thy
   1.118 + of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy
   1.119    | NONE => thy;
   1.120  
   1.121  fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
   1.122 @@ -571,7 +573,7 @@
   1.123  fun add_case thm thy =
   1.124    let
   1.125      val (c, (k, case_pats)) = Code_Unit.case_cert thm;
   1.126 -    val _ = case filter (is_none o get_datatype_of_constr thy) case_pats
   1.127 +    val _ = case filter_out (is_constr thy) case_pats
   1.128       of [] => ()
   1.129        | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
   1.130      val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
   1.131 @@ -607,7 +609,7 @@
   1.132    in
   1.133      TypeInterpretation.init
   1.134      #> add_del_attribute ("", (add_eqn, del_eqn))
   1.135 -    #> add_simple_attribute ("nbe", add_nonlinear_eqn)
   1.136 +    #> add_simple_attribute ("nbe", add_nbe_eqn)
   1.137      #> add_del_attribute ("inline", (add_inline, del_inline))
   1.138      #> add_del_attribute ("post", (add_post, del_post))
   1.139    end));
   1.140 @@ -621,9 +623,7 @@
   1.141    | apply_functrans thy c [] eqns = eqns
   1.142    | apply_functrans thy c functrans eqns = eqns
   1.143        |> perhaps (perhaps_loop (perhaps_apply functrans))
   1.144 -      |> (map o apfst) (AxClass.unoverload thy)
   1.145 -      |> recheck_eqns_const thy c
   1.146 -      |> (map o apfst) (AxClass.overload thy);
   1.147 +      |> recheck_eqns_const thy c;
   1.148  
   1.149  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   1.150  
   1.151 @@ -634,12 +634,13 @@
   1.152    #> Logic.dest_equals
   1.153    #> snd;
   1.154  
   1.155 -fun preprocess thy functrans c eqns =
   1.156 +fun preprocess thy c eqns =
   1.157    let
   1.158      val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   1.159 +    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   1.160 +      o the_thmproc o the_exec) thy;
   1.161    in
   1.162      eqns
   1.163 -    |> (map o apfst) (AxClass.overload thy)
   1.164      |> apply_functrans thy c functrans
   1.165      |> (map o apfst) (Code_Unit.rewrite_eqn pre)
   1.166      |> (map o apfst) (AxClass.unoverload thy)
   1.167 @@ -677,14 +678,9 @@
   1.168    |> burrow_fst (common_typ_eqns thy);
   1.169  
   1.170  fun these_eqns thy c =
   1.171 -  let
   1.172 -    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   1.173 -      o the_thmproc o the_exec) thy;
   1.174 -  in
   1.175 -    get_eqns thy c
   1.176 -    |> (map o apfst) (Thm.transfer thy)
   1.177 -    |> preprocess thy functrans c
   1.178 -  end;
   1.179 +  get_eqns thy c
   1.180 +  |> (map o apfst) (Thm.transfer thy)
   1.181 +  |> preprocess thy c;
   1.182  
   1.183  fun default_typscheme thy c =
   1.184    let
   1.185 @@ -693,10 +689,10 @@
   1.186      fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
   1.187    in case AxClass.class_of_param thy c
   1.188     of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c))
   1.189 -    | NONE => if is_some (get_datatype_of_constr thy c)
   1.190 +    | NONE => if is_constr thy c
   1.191          then strip_sorts (the_const_typscheme c)
   1.192          else case get_eqns thy c
   1.193 -         of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
   1.194 +         of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm
   1.195            | [] => strip_sorts (the_const_typscheme c) end;
   1.196  
   1.197  end; (*local*)