clarified merge
authorhaftmann
Tue Nov 06 13:12:55 2007 +0100 (2007-11-06)
changeset 25312eb9067371342
parent 25311 aa750e3a581c
child 25313 98a145c9a22f
clarified merge
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Tue Nov 06 13:12:53 2007 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Nov 06 13:12:55 2007 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Florian Haftmann, TU Muenchen
     1.5  
     1.6  Abstract executable content of theory.  Management of data dependent on
     1.7 -executable content.
     1.8 +executable content.  Cache assumes non-concurrent processing of a singly theory.
     1.9  *)
    1.10  
    1.11  signature CODE =
    1.12 @@ -78,9 +78,37 @@
    1.13  structure Code : PRIVATE_CODE =
    1.14  struct
    1.15  
    1.16 -(** preliminaries **)
    1.17 +(** code attributes **)
    1.18 +
    1.19 +structure CodeAttr = TheoryDataFun (
    1.20 +  type T = (string * (Args.T list -> attribute * Args.T list)) list;
    1.21 +  val empty = [];
    1.22 +  val copy = I;
    1.23 +  val extend = I;
    1.24 +  fun merge _ = AList.merge (op =) (K true);
    1.25 +);
    1.26  
    1.27 -(* certificate theorems *)
    1.28 +fun add_attribute (attr as (name, _)) =
    1.29 +  let
    1.30 +    fun add_parser ("", parser) attrs = attrs @ [("", parser)]
    1.31 +      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
    1.32 +    fun error "" = error ("Code attribute already declared")
    1.33 +      | error name = error ("Code attribute " ^ name ^ " already declared")
    1.34 +  in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
    1.35 +    then error name else add_parser attr attrs)
    1.36 +  end;
    1.37 +
    1.38 +val _ =
    1.39 +  let
    1.40 +    val code_attr = Attrib.syntax (Scan.peek (fn context =>
    1.41 +      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
    1.42 +  in
    1.43 +    Context.add_setup (Attrib.add_attributes
    1.44 +      [("code", code_attr, "declare theorems for code generation")])
    1.45 +  end;
    1.46 +
    1.47 +
    1.48 +(** certificate theorems **)
    1.49  
    1.50  fun string_of_lthms r = case Susp.peek r
    1.51   of SOME thms => (map string_of_thm o rev) thms
    1.52 @@ -97,27 +125,8 @@
    1.53          val thy_ref = Theory.check_thy thy;
    1.54        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    1.55  
    1.56 -fun merge' _ ([], []) = (false, [])
    1.57 -  | merge' _ ([], ys) = (true, ys)
    1.58 -  | merge' eq (xs, ys) = fold_rev
    1.59 -      (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs);
    1.60  
    1.61 -fun merge_alist eq_key eq (xys as (xs, ys)) =
    1.62 -  if eq_list (eq_pair eq_key eq) (xs, ys)
    1.63 -  then (false, xs)
    1.64 -  else (true, AList.merge eq_key eq xys);
    1.65 -
    1.66 -val merge_thms = merge' Thm.eq_thm_prop;
    1.67 -
    1.68 -fun merge_lthms (r1, r2) =
    1.69 -  if Susp.same (r1, r2)
    1.70 -    then (false, r1)
    1.71 -  else case Susp.peek r1
    1.72 -   of SOME [] => (true, r2)
    1.73 -    | _ => case Susp.peek r2
    1.74 -       of SOME [] => (true, r1)
    1.75 -        | _ => (apsnd (Susp.delay o K)) (merge_thms (Susp.force r1, Susp.force r2));
    1.76 -
    1.77 +(** logical and syntactical specification of executable code **)
    1.78  
    1.79  (* pairs of (selected, deleted) defining equations *)
    1.80  
    1.81 @@ -152,108 +161,72 @@
    1.82  
    1.83  fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
    1.84  
    1.85 -fun merge_sdthms ((sels1, dels1), (sels2, dels2)) =
    1.86 +
    1.87 +(* fundamental melting operations *)
    1.88 +
    1.89 +fun melt _ ([], []) = (false, [])
    1.90 +  | melt _ ([], ys) = (true, ys)
    1.91 +  | melt eq (xs, ys) = fold_rev
    1.92 +      (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs);
    1.93 +
    1.94 +fun melt_alist eq_key eq (xys as (xs, ys)) =
    1.95 +  if eq_list (eq_pair eq_key eq) (xs, ys)
    1.96 +  then (false, xs)
    1.97 +  else (true, AList.merge eq_key eq xys);
    1.98 +
    1.99 +val melt_thms = melt Thm.eq_thm_prop;
   1.100 +
   1.101 +fun melt_lthms (r1, r2) =
   1.102 +  if Susp.same (r1, r2)
   1.103 +    then (false, r1)
   1.104 +  else case Susp.peek r1
   1.105 +   of SOME [] => (true, r2)
   1.106 +    | _ => case Susp.peek r2
   1.107 +       of SOME [] => (true, r1)
   1.108 +        | _ => (apsnd (Susp.delay o K)) (melt_thms (Susp.force r1, Susp.force r2));
   1.109 +
   1.110 +fun melt_sdthms ((sels1, dels1), (sels2, dels2)) =
   1.111    let
   1.112 -    val (dels_t, dels) = merge_thms (dels1, dels2);
   1.113 +    val (dels_t, dels) = melt_thms (dels1, dels2);
   1.114    in if dels_t
   1.115      then let
   1.116 -      val (_, sels) = merge_thms
   1.117 +      val (_, sels) = melt_thms
   1.118          (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2);
   1.119 -      val (_, dels) = merge_thms
   1.120 +      val (_, dels) = melt_thms
   1.121          (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2);
   1.122      in (true, ((Susp.delay o K) sels, dels)) end
   1.123      else let
   1.124 -      val (sels_t, sels) = merge_lthms (sels1, sels2);
   1.125 +      val (sels_t, sels) = melt_lthms (sels1, sels2);
   1.126      in (sels_t, (sels, dels)) end
   1.127    end;
   1.128  
   1.129  
   1.130 -(* code attributes *)
   1.131 -
   1.132 -structure CodeAttr = TheoryDataFun (
   1.133 -  type T = (string * (Args.T list -> attribute * Args.T list)) list;
   1.134 -  val empty = [];
   1.135 -  val copy = I;
   1.136 -  val extend = I;
   1.137 -  fun merge _ = AList.merge (op =) (K true);
   1.138 -);
   1.139 -
   1.140 -fun add_attribute (attr as (name, _)) =
   1.141 -  let
   1.142 -    fun add_parser ("", parser) attrs = attrs @ [("", parser)]
   1.143 -      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
   1.144 -    fun error "" = error ("Code attribute already declared")
   1.145 -      | error name = error ("Code attribute " ^ name ^ " already declared")
   1.146 -  in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
   1.147 -    then error name else add_parser attr attrs)
   1.148 -  end;
   1.149 -
   1.150 -val _ =
   1.151 -  let
   1.152 -    val code_attr = Attrib.syntax (Scan.peek (fn context =>
   1.153 -      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
   1.154 -  in
   1.155 -    Context.add_setup (Attrib.add_attributes
   1.156 -      [("code", code_attr, "declare theorems for code generation")])
   1.157 -  end;
   1.158 -
   1.159 -
   1.160 -
   1.161 -(** exeuctable content **)
   1.162 +(* specification data *)
   1.163  
   1.164 -datatype thmproc = Preproc of {
   1.165 -  inlines: thm list,
   1.166 -  inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
   1.167 -  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
   1.168 -  posts: thm list
   1.169 -};
   1.170 -
   1.171 -fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
   1.172 -  Preproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
   1.173 -    posts = posts };
   1.174 -fun map_thmproc f (Preproc { inlines, inline_procs, preprocs, posts }) =
   1.175 -  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
   1.176 -fun merge_thmproc (Preproc { inlines = inlines1, inline_procs = inline_procs1,
   1.177 -    preprocs = preprocs1, posts = posts1 },
   1.178 -  Preproc { inlines = inlines2, inline_procs = inline_procs2,
   1.179 -      preprocs = preprocs2, posts= posts2 }) =
   1.180 -    let
   1.181 -      val (touched1, inlines) = merge_thms (inlines1, inlines2);
   1.182 -      val (touched2, inline_procs) = merge_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
   1.183 -      val (touched3, preprocs) = merge_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
   1.184 -      val (_, posts) = merge_thms (posts1, posts2);
   1.185 -    in (touched1 orelse touched2 orelse touched3,
   1.186 -      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
   1.187 -
   1.188 -fun join_func_thms (tabs as (tab1, tab2)) =
   1.189 +fun melt_funcs tabs =
   1.190    let
   1.191 -    val cs1 = Symtab.keys tab1;
   1.192 -    val cs2 = Symtab.keys tab2;
   1.193 -    val cs' = filter (member (op =) cs2) cs1;
   1.194 -    val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
   1.195 -    val cs''' = ref [] : string list ref;
   1.196 -    fun merge c x = let val (touched, thms') = merge_sdthms x in
   1.197 -      (if touched then cs''' := cons c (!cs''') else (); thms') end;
   1.198 -  in (cs'' @ !cs''', Symtab.join merge tabs) end;
   1.199 +    val tab' = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b)) tabs;
   1.200 +    val touched = Symtab.fold (fn (c, (true, _)) => insert (op =) c | _ => I) tab' [];
   1.201 +  in (touched, tab') end;
   1.202  
   1.203  val eq_string = op = : string * string -> bool;
   1.204  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   1.205    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
   1.206      andalso gen_eq_set (eq_fst eq_string) (cs1, cs2);
   1.207 -fun merge_dtyps (tabs as (tab1, tab2)) =
   1.208 +fun melt_dtyps (tabs as (tab1, tab2)) =
   1.209    let
   1.210      val tycos1 = Symtab.keys tab1;
   1.211      val tycos2 = Symtab.keys tab2;
   1.212      val tycos' = filter (member eq_string tycos2) tycos1;
   1.213 -    val new_types = not (gen_eq_set (op =) (tycos1, tycos2));
   1.214 -    val diff_types = not (gen_eq_set (eq_pair (op =) eq_dtyp)
   1.215 +    val touched = not (gen_eq_set (op =) (tycos1, tycos2)
   1.216 +      andalso gen_eq_set (eq_pair (op =) eq_dtyp)
   1.217        (AList.make (the o Symtab.lookup tab1) tycos',
   1.218         AList.make (the o Symtab.lookup tab2) tycos'));
   1.219      fun join _ (cos as (_, cos2)) = if eq_dtyp cos
   1.220        then raise Symtab.SAME else cos2;
   1.221 -  in ((new_types, diff_types), Symtab.join join tabs) end;
   1.222 +  in (touched, Symtab.join join tabs) end;
   1.223  
   1.224 -fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
   1.225 +fun melt_cases ((cases1, undefs1), (cases2, undefs2)) =
   1.226    let
   1.227      val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2)
   1.228        @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1);
   1.229 @@ -266,7 +239,7 @@
   1.230    end;
   1.231  
   1.232  datatype spec = Spec of {
   1.233 -  funcs: sdthms Symtab.table,
   1.234 +  funcs: (bool * sdthms) Symtab.table,
   1.235    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
   1.236    cases: (int * string list) Symtab.table * unit Symtab.table
   1.237  };
   1.238 @@ -275,16 +248,43 @@
   1.239    Spec { funcs = funcs, dtyps = dtyps, cases = cases };
   1.240  fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
   1.241    mk_spec (f (funcs, (dtyps, cases)));
   1.242 -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
   1.243 +fun melt_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
   1.244    Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
   1.245    let
   1.246 -    val (touched_cs, funcs) = join_func_thms (funcs1, funcs2);
   1.247 -    val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
   1.248 -    val (touched_cases, cases) = merge_cases (cases1, cases2);
   1.249 -    val touched = if new_types orelse diff_types then NONE else
   1.250 -      SOME (fold (insert (op =)) touched_cases touched_cs);
   1.251 +    val (touched_funcs, funcs) = melt_funcs (funcs1, funcs2);
   1.252 +    val (touched_dtyps, dtyps) = melt_dtyps (dtyps1, dtyps2);
   1.253 +    val (touched_cases, cases) = melt_cases (cases1, cases2);
   1.254 +    val touched = if touched_dtyps then NONE else
   1.255 +      SOME (fold (insert (op =)) touched_cases touched_funcs);
   1.256    in (touched, mk_spec (funcs, (dtyps, cases))) end;
   1.257  
   1.258 +
   1.259 +(* pre- and postprocessor *)
   1.260 +
   1.261 +datatype thmproc = Thmproc of {
   1.262 +  inlines: thm list,
   1.263 +  inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
   1.264 +  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
   1.265 +  posts: thm list
   1.266 +};
   1.267 +
   1.268 +fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
   1.269 +  Thmproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
   1.270 +    posts = posts };
   1.271 +fun map_thmproc f (Thmproc { inlines, inline_procs, preprocs, posts }) =
   1.272 +  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
   1.273 +fun melt_thmproc (Thmproc { inlines = inlines1, inline_procs = inline_procs1,
   1.274 +    preprocs = preprocs1, posts = posts1 },
   1.275 +  Thmproc { inlines = inlines2, inline_procs = inline_procs2,
   1.276 +      preprocs = preprocs2, posts= posts2 }) =
   1.277 +    let
   1.278 +      val (touched1, inlines) = melt_thms (inlines1, inlines2);
   1.279 +      val (touched2, inline_procs) = melt_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
   1.280 +      val (touched3, preprocs) = melt_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
   1.281 +      val (_, posts) = melt_thms (posts1, posts2);
   1.282 +    in (touched1 orelse touched2 orelse touched3,
   1.283 +      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
   1.284 +
   1.285  datatype exec = Exec of {
   1.286    thmproc: thmproc,
   1.287    spec: spec
   1.288 @@ -294,17 +294,17 @@
   1.289    Exec { thmproc = thmproc, spec = spec };
   1.290  fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
   1.291    mk_exec (f (thmproc, spec));
   1.292 -fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
   1.293 +fun melt_exec (Exec { thmproc = thmproc1, spec = spec1 },
   1.294    Exec { thmproc = thmproc2, spec = spec2 }) =
   1.295    let
   1.296 -    val (touched', thmproc) = merge_thmproc (thmproc1, thmproc2);
   1.297 -    val (touched_cs, spec) = merge_spec (spec1, spec2);
   1.298 +    val (touched', thmproc) = melt_thmproc (thmproc1, thmproc2);
   1.299 +    val (touched_cs, spec) = melt_spec (spec1, spec2);
   1.300      val touched = if touched' then NONE else touched_cs;
   1.301    in (touched, mk_exec (thmproc, spec)) end;
   1.302  val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
   1.303    mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
   1.304  
   1.305 -fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
   1.306 +fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
   1.307  fun the_spec (Exec { spec = Spec x, ...}) = x;
   1.308  val the_funcs = #funcs o the_spec;
   1.309  val the_dtyps = #dtyps o the_spec;
   1.310 @@ -357,7 +357,7 @@
   1.311  end; (*local*)
   1.312  
   1.313  
   1.314 -(* theory store *)
   1.315 +(** theory store **)
   1.316  
   1.317  local
   1.318  
   1.319 @@ -371,7 +371,7 @@
   1.320    val extend = copy;
   1.321    fun merge pp ((exec1, data1), (exec2, data2)) =
   1.322      let
   1.323 -      val (touched, exec) = merge_exec (exec1, exec2);
   1.324 +      val (touched, exec) = melt_exec (exec1, exec2);
   1.325        val data1' = invoke_purge_all NONE touched (! data1);
   1.326        val data2' = invoke_purge_all NONE touched (! data2);
   1.327        val data = invoke_merge_all pp (data1', data2');
   1.328 @@ -452,6 +452,7 @@
   1.329      val preprocs = (map fst o #preprocs o the_thmproc) exec;
   1.330      val funs = the_funcs exec
   1.331        |> Symtab.dest
   1.332 +      |> (map o apsnd) snd
   1.333        |> (map o apfst) (CodeUnit.string_of_const thy)
   1.334        |> sort (string_ord o pairself fst);
   1.335      val dtyps = the_dtyps exec
   1.336 @@ -549,7 +550,7 @@
   1.337      val funcs = classparams
   1.338        |> map (fn c => Class.inst_const thy (c, tyco))
   1.339        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
   1.340 -      |> (map o Option.map) (Susp.force o fst)
   1.341 +      |> (map o Option.map) (Susp.force o fst o snd)
   1.342        |> maps these
   1.343        |> map (Thm.transfer thy)
   1.344      fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
   1.345 @@ -710,7 +711,7 @@
   1.346        else ();
   1.347    in
   1.348      (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
   1.349 -      (c, (Susp.value [], [])) (add_thm func)) thy
   1.350 +      (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy
   1.351    end;
   1.352  
   1.353  fun add_liberal_func thm thy =
   1.354 @@ -722,7 +723,7 @@
   1.355            then thy
   1.356            else map_exec_purge (SOME [c]) (map_funcs
   1.357              (Symtab.map_default
   1.358 -              (c, (Susp.value [], [])) (add_thm func))) thy
   1.359 +              (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
   1.360          end
   1.361      | NONE => thy;
   1.362  
   1.363 @@ -735,7 +736,7 @@
   1.364            then thy
   1.365            else map_exec_purge (SOME [c]) (map_funcs
   1.366            (Symtab.map_default
   1.367 -            (c, (Susp.value [], [])) (add_thm func))) thy
   1.368 +            (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
   1.369          end
   1.370      | NONE => thy;
   1.371  
   1.372 @@ -744,7 +745,7 @@
   1.373     of SOME func => let
   1.374            val c = const_of_func thy func;
   1.375          in map_exec_purge (SOME [c]) (map_funcs
   1.376 -          (Symtab.map_entry c (del_thm func))) thy
   1.377 +          (Symtab.map_entry c (apsnd (del_thm func)))) thy
   1.378          end
   1.379      | NONE => thy;
   1.380  
   1.381 @@ -754,8 +755,9 @@
   1.382        (*FIXME must check compatibility with sort algebra;
   1.383          alas, naive checking results in non-termination!*)
   1.384    in
   1.385 -    map_exec_purge (SOME [const]) (map_funcs (Symtab.map_default (const, (Susp.value [], []))
   1.386 -      (add_lthms lthms'))) thy
   1.387 +    map_exec_purge (SOME [const])
   1.388 +      (map_funcs (Symtab.map_default (const, (false, (Susp.value [], [])))
   1.389 +      (apsnd (add_lthms lthms')))) thy
   1.390    end;
   1.391  
   1.392  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   1.393 @@ -925,7 +927,7 @@
   1.394  
   1.395  fun get_funcs thy const =
   1.396    Symtab.lookup ((the_funcs o the_exec) thy) const
   1.397 -  |> Option.map (Susp.force o fst)
   1.398 +  |> Option.map (Susp.force o fst o snd)
   1.399    |> these
   1.400    |> map (Thm.transfer thy);
   1.401