src/Pure/Isar/code.ML
changeset 28143 e5c6c4aac52c
parent 28054 2b84d34c5d02
child 28350 715163ec93c0
     1.1 --- a/src/Pure/Isar/code.ML	Fri Sep 05 06:50:20 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Sep 05 06:50:22 2008 +0200
     1.3 @@ -113,11 +113,9 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(** certificate theorems **)
     1.8 +(** logical and syntactical specification of executable code **)
     1.9  
    1.10 -fun string_of_lthms r = case Susp.peek r
    1.11 - of SOME thms => (map Display.string_of_thm o rev) thms
    1.12 -  | NONE => ["[...]"];
    1.13 +(* defining equations with default flag and lazy theorems *)
    1.14  
    1.15  fun pretty_lthms ctxt r = case Susp.peek r
    1.16   of SOME thms => map (ProofContext.pretty_thm ctxt) thms
    1.17 @@ -130,15 +128,11 @@
    1.18          val thy_ref = Theory.check_thy thy;
    1.19        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    1.20  
    1.21 -
    1.22 -(** logical and syntactical specification of executable code **)
    1.23 -
    1.24 -(* pairs of (selected, deleted) defining equations *)
    1.25 -
    1.26 -type sdthms = thm list Susp.T * thm list;
    1.27 -
    1.28 -fun add_drop_redundant thm (sels, dels) =
    1.29 +fun add_drop_redundant verbose thm thms =
    1.30    let
    1.31 +    fun warn thm' = (if verbose
    1.32 +      then warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm')
    1.33 +      else (); true);
    1.34      val thy = Thm.theory_of_thm thm;
    1.35      val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    1.36      val args = args_of thm;
    1.37 @@ -146,76 +140,40 @@
    1.38        | matches (Var _ :: xs) [] = matches xs []
    1.39        | matches (_ :: _) [] = false
    1.40        | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
    1.41 -    fun drop thm' = not (matches args (args_of thm'))
    1.42 -      orelse (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false);
    1.43 -    val (keeps, drops) = List.partition drop sels;
    1.44 -  in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end;
    1.45 -
    1.46 -fun add_thm thm (sels, dels) =
    1.47 -  apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
    1.48 +    fun drop thm' = matches args (args_of thm') andalso warn thm';
    1.49 +  in thm :: filter_out drop thms end;
    1.50  
    1.51 -fun add_lthms lthms (sels, []) =
    1.52 -      (Susp.delay (fn () => fold add_drop_redundant
    1.53 -        (Susp.force lthms) (Susp.force sels, []) |> fst), [])
    1.54 -        (*FIXME*)
    1.55 -  | add_lthms lthms (sels, dels) =
    1.56 -      fold add_thm (Susp.force lthms) (sels, dels);
    1.57 -
    1.58 -fun del_thm thm (sels, dels) =
    1.59 -  (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels);
    1.60 -
    1.61 -fun del_thms (sels, dels) =
    1.62 -  let
    1.63 -    val all_sels = Susp.force sels;
    1.64 -  in (Susp.value [], rev all_sels @ dels) end;
    1.65 -
    1.66 -fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
    1.67 +fun add_thm _ thm (false, thms) = (false, Susp.value (add_drop_redundant true thm (Susp.force thms)))
    1.68 +  | add_thm true thm (true, thms) = (true, Susp.value (Susp.force thms @ [thm]))
    1.69 +  | add_thm false thm (true, thms) = (false, Susp.value [thm]);
    1.70  
    1.71 -fun melt _ ([], []) = (false, [])
    1.72 -  | melt _ ([], ys) = (true, ys)
    1.73 -  | melt eq (xs, ys) = fold_rev
    1.74 -      (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs);
    1.75 +fun add_lthms lthms _ = (false, lthms);
    1.76  
    1.77 -val melt_thms = melt Thm.eq_thm_prop;
    1.78 +fun del_thm thm = apsnd (Susp.value o remove Thm.eq_thm_prop thm o Susp.force);
    1.79  
    1.80 -fun melt_lthms (r1, r2) =
    1.81 -  if Susp.same (r1, r2)
    1.82 -    then (false, r1)
    1.83 -  else case Susp.peek r1
    1.84 -   of SOME [] => (true, r2)
    1.85 -    | _ => case Susp.peek r2
    1.86 -       of SOME [] => (true, r1)
    1.87 -        | _ => (apsnd (Susp.delay o K)) (melt_thms (Susp.force r1, Susp.force r2));
    1.88 -
    1.89 -fun melt_sdthms ((sels1, dels1), (sels2, dels2)) =
    1.90 -  let
    1.91 -    val (dels_t, dels) = melt_thms (dels1, dels2);
    1.92 -  in if dels_t
    1.93 -    then let
    1.94 -      val (_, sels) = melt_thms
    1.95 -        (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2);
    1.96 -      val (_, dels) = melt_thms
    1.97 -        (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2);
    1.98 -    in ((Susp.delay o K) sels, dels) end
    1.99 -    else let
   1.100 -      val (_, sels) = melt_lthms (sels1, sels2);
   1.101 -    in (sels, dels) end
   1.102 -  end;
   1.103 +fun merge_defthms ((true, _), defthms2) = defthms2
   1.104 +  | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1
   1.105 +  | merge_defthms ((false, _), defthms2 as (false, _)) = defthms2;
   1.106  
   1.107  
   1.108 -(* specification data *)
   1.109 +(* syntactic datatypes *)
   1.110  
   1.111  val eq_string = op = : string * string -> bool;
   1.112 +
   1.113  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   1.114    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
   1.115      andalso gen_eq_set (eq_fst eq_string) (cs1, cs2);
   1.116 +
   1.117  fun merge_dtyps (tabs as (tab1, tab2)) =
   1.118    let
   1.119      fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2;
   1.120    in Symtab.join join tabs end;
   1.121  
   1.122 +
   1.123 +(* specification data *)
   1.124 +
   1.125  datatype spec = Spec of {
   1.126 -  funcs: sdthms Symtab.table,
   1.127 +  funcs: (bool * thm list Susp.T) Symtab.table,
   1.128    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
   1.129    cases: (int * string list) Symtab.table * unit Symtab.table
   1.130  };
   1.131 @@ -227,7 +185,7 @@
   1.132  fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = (cases1, undefs1) },
   1.133    Spec { funcs = funcs2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
   1.134    let
   1.135 -    val funcs = Symtab.join (K melt_sdthms) (funcs1, funcs2);
   1.136 +    val funcs = Symtab.join (K merge_defthms) (funcs1, funcs2);
   1.137      val dtyps = merge_dtyps (dtyps1, dtyps2);
   1.138      val cases = (Symtab.merge (K true) (cases1, cases2),
   1.139        Symtab.merge (K true) (undefs1, undefs2));
   1.140 @@ -259,6 +217,9 @@
   1.141    spec: spec
   1.142  };
   1.143  
   1.144 +
   1.145 +(* code setup data *)
   1.146 +
   1.147  fun mk_exec (thmproc, spec) =
   1.148    Exec { thmproc = thmproc, spec = spec };
   1.149  fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
   1.150 @@ -398,9 +359,9 @@
   1.151    let
   1.152      val ctxt = ProofContext.init thy;
   1.153      val exec = the_exec thy;
   1.154 -    fun pretty_func (s, lthms) =
   1.155 +    fun pretty_func (s, (_, lthms)) =
   1.156        (Pretty.block o Pretty.fbreaks) (
   1.157 -        Pretty.str s :: pretty_sdthms ctxt lthms
   1.158 +        Pretty.str s :: pretty_lthms ctxt lthms
   1.159        );
   1.160      fun pretty_dtyp (s, []) =
   1.161            Pretty.str s
   1.162 @@ -518,9 +479,9 @@
   1.163      val funcs = classparams
   1.164        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
   1.165        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
   1.166 -      |> (map o Option.map) (Susp.force o fst)
   1.167 +      |> (map o Option.map) (Susp.force o snd)
   1.168        |> maps these
   1.169 -      |> map (Thm.transfer thy)
   1.170 +      |> map (Thm.transfer thy);
   1.171      fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
   1.172        | sorts_of tys = map (snd o dest_TVar) tys;
   1.173      val sorts = map (sorts_of o Sign.const_typargs thy o const_of thy) funcs;
   1.174 @@ -643,8 +604,7 @@
   1.175  val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func);
   1.176  val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func);
   1.177  
   1.178 -end;
   1.179 -
   1.180 +end; (*local*)
   1.181  
   1.182  
   1.183  (** interfaces and attributes **)
   1.184 @@ -681,70 +641,49 @@
   1.185  
   1.186  val is_undefined = Symtab.defined o snd o the_cases o the_exec;
   1.187  
   1.188 -fun add_func thm thy =
   1.189 -  let
   1.190 -    val func = mk_func thm;
   1.191 -    val c = const_of_func thy func;
   1.192 -    val _ = if (is_some o AxClass.class_of_param thy) c
   1.193 -      then error ("Rejected polymorphic equation for overloaded constant:\n"
   1.194 -        ^ Display.string_of_thm thm)
   1.195 -      else ();
   1.196 -    val _ = if (is_some o get_datatype_of_constr thy) c
   1.197 -      then error ("Rejected equation for datatype constructor:\n"
   1.198 -        ^ Display.string_of_thm func)
   1.199 -      else ();
   1.200 -  in
   1.201 -    (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
   1.202 -      (c, (Susp.value [], [])) (add_thm func)) thy
   1.203 -  end;
   1.204 -
   1.205 -fun add_liberal_func thm thy =
   1.206 -  case mk_liberal_func thm
   1.207 -   of SOME func => let
   1.208 -          val c = const_of_func thy func
   1.209 -        in if (is_some o AxClass.class_of_param thy) c
   1.210 -          orelse (is_some o get_datatype_of_constr thy) c
   1.211 -          then thy
   1.212 -          else map_exec_purge (SOME [c]) (map_funcs
   1.213 -            (Symtab.map_default
   1.214 -              (c, (Susp.value [], [])) (add_thm func))) thy
   1.215 +fun gen_add_func strict default thm thy =
   1.216 +  case (if strict then SOME o mk_func else mk_liberal_func) thm
   1.217 +   of SOME func =>
   1.218 +        let
   1.219 +          val c = const_of_func thy func;
   1.220 +          val _ = if strict andalso (is_some o AxClass.class_of_param thy) c
   1.221 +            then error ("Rejected polymorphic equation for overloaded constant:\n"
   1.222 +              ^ Display.string_of_thm thm)
   1.223 +            else ();
   1.224 +          val _ = if strict andalso (is_some o get_datatype_of_constr thy) c
   1.225 +            then error ("Rejected equation for datatype constructor:\n"
   1.226 +              ^ Display.string_of_thm func)
   1.227 +            else ();
   1.228 +        in
   1.229 +          (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
   1.230 +            (c, (true, Susp.value [])) (add_thm default func)) thy
   1.231          end
   1.232      | NONE => thy;
   1.233  
   1.234 -fun add_default_func thm thy =
   1.235 -  case mk_default_func thm
   1.236 -   of SOME func => let
   1.237 -          val c = const_of_func thy func
   1.238 -        in if (is_some o AxClass.class_of_param thy) c
   1.239 -          orelse (is_some o get_datatype_of_constr thy) c
   1.240 -          then thy
   1.241 -          else map_exec_purge (SOME [c]) (map_funcs
   1.242 -          (Symtab.map_default
   1.243 -            (c, (Susp.value [], [])) (add_thm func))) thy
   1.244 -        end
   1.245 -    | NONE => thy;
   1.246 +val add_func = gen_add_func true false;
   1.247 +val add_liberal_func = gen_add_func false false;
   1.248 +val add_default_func = gen_add_func false true;
   1.249  
   1.250 -fun del_func thm thy =
   1.251 -  case mk_liberal_func thm
   1.252 -   of SOME func => let
   1.253 -          val c = const_of_func thy func;
   1.254 -        in map_exec_purge (SOME [c]) (map_funcs
   1.255 -          (Symtab.map_entry c (del_thm func))) thy
   1.256 -        end
   1.257 -    | NONE => thy;
   1.258 +fun del_func thm thy = case mk_liberal_func thm
   1.259 + of SOME func => let
   1.260 +        val c = const_of_func thy func;
   1.261 +      in map_exec_purge (SOME [c]) (map_funcs
   1.262 +        (Symtab.map_entry c (del_thm func))) thy
   1.263 +      end
   1.264 +  | NONE => thy;
   1.265  
   1.266 -fun del_funcs const = map_exec_purge (SOME [const])
   1.267 -  (map_funcs (Symtab.map_entry const del_thms));
   1.268 +fun del_funcs c = map_exec_purge (SOME [c])
   1.269 +  (map_funcs (Symtab.map_entry c (K (false, Susp.value []))));
   1.270  
   1.271 -fun add_funcl (const, lthms) thy =
   1.272 +fun add_funcl (c, lthms) thy =
   1.273    let
   1.274 -    val lthms' = certificate thy (fn thy => certify_const thy const) lthms;
   1.275 +    val lthms' = certificate thy (fn thy => certify_const thy c) lthms;
   1.276        (*FIXME must check compatibility with sort algebra;
   1.277          alas, naive checking results in non-termination!*)
   1.278    in
   1.279 -    map_exec_purge (SOME [const])
   1.280 -      (map_funcs (Symtab.map_default (const, (Susp.value [], []))
   1.281 -      (add_lthms lthms'))) thy
   1.282 +    map_exec_purge (SOME [c])
   1.283 +      (map_funcs (Symtab.map_default (c, (true, Susp.value []))
   1.284 +        (add_lthms lthms'))) thy
   1.285    end;
   1.286  
   1.287  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   1.288 @@ -906,7 +845,7 @@
   1.289  
   1.290  fun get_funcs thy const =
   1.291    Symtab.lookup ((the_funcs o the_exec) thy) const
   1.292 -  |> Option.map (Susp.force o fst)
   1.293 +  |> Option.map (Susp.force o snd)
   1.294    |> these
   1.295    |> map (Thm.transfer thy);
   1.296  
   1.297 @@ -953,9 +892,4 @@
   1.298  
   1.299  end;
   1.300  
   1.301 -structure Code : CODE =
   1.302 -struct
   1.303 -
   1.304 -open Code;
   1.305 -
   1.306 -end;
   1.307 +structure Code : CODE = struct open Code; end;