8 |
8 |
9 signature CODE = |
9 signature CODE = |
10 sig |
10 sig |
11 val add_eqn: thm -> theory -> theory |
11 val add_eqn: thm -> theory -> theory |
12 val add_nonlinear_eqn: thm -> theory -> theory |
12 val add_nonlinear_eqn: thm -> theory -> theory |
13 val add_liberal_eqn: thm -> theory -> theory |
|
14 val add_default_eqn: thm -> theory -> theory |
13 val add_default_eqn: thm -> theory -> theory |
15 val add_default_eqn_attr: Attrib.src |
14 val add_default_eqn_attr: Attrib.src |
16 val del_eqn: thm -> theory -> theory |
15 val del_eqn: thm -> theory -> theory |
17 val del_eqns: string -> theory -> theory |
16 val del_eqns: string -> theory -> theory |
18 val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory |
17 val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory |
19 val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory |
18 val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory |
20 val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory |
19 val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory |
21 val add_inline: thm -> theory -> theory |
20 val add_inline: thm -> theory -> theory |
22 val del_inline: thm -> theory -> theory |
|
23 val add_post: thm -> theory -> theory |
|
24 val del_post: thm -> theory -> theory |
|
25 val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory |
21 val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory |
26 val del_functrans: string -> theory -> theory |
22 val del_functrans: string -> theory -> theory |
27 val add_datatype: (string * typ) list -> theory -> theory |
23 val add_datatype: (string * typ) list -> theory -> theory |
28 val add_datatype_cmd: string list -> theory -> theory |
24 val add_datatype_cmd: string list -> theory -> theory |
29 val type_interpretation: |
25 val type_interpretation: |
147 |
146 |
148 fun add_lthms lthms _ = (false, lthms); |
147 fun add_lthms lthms _ = (false, lthms); |
149 |
148 |
150 fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true)); |
149 fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true)); |
151 |
150 |
152 fun merge_defthms ((true, _), defthms2) = defthms2 |
|
153 | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1 |
|
154 | merge_defthms ((false, _), defthms2 as (false, _)) = defthms2; |
|
155 |
|
156 |
|
157 (* syntactic datatypes *) |
|
158 |
|
159 val eq_string = op = : string * string -> bool; |
|
160 |
|
161 fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = |
|
162 gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) |
|
163 andalso gen_eq_set (eq_fst eq_string) (cs1, cs2); |
|
164 |
|
165 fun merge_dtyps (tabs as (tab1, tab2)) = |
|
166 let |
|
167 fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2; |
|
168 in Symtab.join join tabs end; |
|
169 |
|
170 |
151 |
171 (* specification data *) |
152 (* specification data *) |
172 |
153 |
173 datatype spec = Spec of { |
154 datatype spec = Spec of { |
174 eqns: (bool * (thm * bool) list Lazy.T) Symtab.table, |
155 concluded_history: bool, |
175 dtyps: ((string * sort) list * (string * typ list) list) Symtab.table, |
156 eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table |
|
157 (*with explicit history*), |
|
158 dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table |
|
159 (*with explicit history*), |
176 cases: (int * string list) Symtab.table * unit Symtab.table |
160 cases: (int * string list) Symtab.table * unit Symtab.table |
177 }; |
161 }; |
178 |
162 |
179 fun mk_spec (eqns, (dtyps, cases)) = |
163 fun mk_spec ((concluded_history, eqns), (dtyps, cases)) = |
180 Spec { eqns = eqns, dtyps = dtyps, cases = cases }; |
164 Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases }; |
181 fun map_spec f (Spec { eqns = eqns, dtyps = dtyps, cases = cases }) = |
165 fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns, |
182 mk_spec (f (eqns, (dtyps, cases))); |
166 dtyps = dtyps, cases = cases }) = |
183 fun merge_spec (Spec { eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) }, |
167 mk_spec (f ((concluded_history, eqns), (dtyps, cases))); |
184 Spec { eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) = |
168 fun merge_spec (Spec { concluded_history = _, eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) }, |
185 let |
169 Spec { concluded_history = _, eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) = |
186 val eqns = Symtab.join (K merge_defthms) (eqns1, eqns2); |
170 let |
187 val dtyps = merge_dtyps (dtyps1, dtyps2); |
171 fun merge_eqns ((_, history1), (_, history2)) = |
|
172 let |
|
173 val raw_history = AList.merge (op =) (K true) (history1, history2) |
|
174 val filtered_history = filter_out (fst o snd) raw_history |
|
175 val history = if null filtered_history |
|
176 then raw_history else filtered_history; |
|
177 in ((false, (snd o hd) history), history) end; |
|
178 val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2); |
|
179 val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2); |
188 val cases = (Symtab.merge (K true) (cases1, cases2), |
180 val cases = (Symtab.merge (K true) (cases1, cases2), |
189 Symtab.merge (K true) (undefs1, undefs2)); |
181 Symtab.merge (K true) (undefs1, undefs2)); |
190 in mk_spec (eqns, (dtyps, cases)) end; |
182 in mk_spec ((false, eqns), (dtyps, cases)) end; |
191 |
183 |
192 |
184 |
193 (* pre- and postprocessor *) |
185 (* pre- and postprocessor *) |
194 |
186 |
195 datatype thmproc = Thmproc of { |
187 datatype thmproc = Thmproc of { |
227 let |
219 let |
228 val thmproc = merge_thmproc (thmproc1, thmproc2); |
220 val thmproc = merge_thmproc (thmproc1, thmproc2); |
229 val spec = merge_spec (spec1, spec2); |
221 val spec = merge_spec (spec1, spec2); |
230 in mk_exec (thmproc, spec) end; |
222 in mk_exec (thmproc, spec) end; |
231 val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []), |
223 val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []), |
232 mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))); |
224 mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty)))); |
233 |
225 |
234 fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x; |
226 fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x; |
235 fun the_spec (Exec { spec = Spec x, ...}) = x; |
227 fun the_spec (Exec { spec = Spec x, ...}) = x; |
236 val the_eqns = #eqns o the_spec; |
228 val the_eqns = #eqns o the_spec; |
237 val the_dtyps = #dtyps o the_spec; |
229 val the_dtyps = #dtyps o the_spec; |
238 val the_cases = #cases o the_spec; |
230 val the_cases = #cases o the_spec; |
239 val map_thmproc = map_exec o apfst o map_thmproc; |
231 val map_thmproc = map_exec o apfst o map_thmproc; |
240 val map_eqns = map_exec o apsnd o map_spec o apfst; |
232 val map_concluded_history = map_exec o apsnd o map_spec o apfst o apfst; |
|
233 val map_eqns = map_exec o apsnd o map_spec o apfst o apsnd; |
241 val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst; |
234 val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst; |
242 val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd; |
235 val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd; |
243 |
236 |
244 |
237 |
245 (* data slots dependent on executable content *) |
238 (* data slots dependent on executable content *) |
322 CodeData.map (fn (exec, data) => (f exec, ref (case touched |
313 CodeData.map (fn (exec, data) => (f exec, ref (case touched |
323 of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data) |
314 of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data) |
324 | NONE => empty_data))) thy; |
315 | NONE => empty_data))) thy; |
325 |
316 |
326 val purge_data = (CodeData.map o apsnd) (K (ref empty_data)); |
317 val purge_data = (CodeData.map o apsnd) (K (ref empty_data)); |
|
318 |
|
319 |
|
320 (* tackling equation history *) |
|
321 |
|
322 fun get_eqns thy c = |
|
323 Symtab.lookup ((the_eqns o the_exec) thy) c |
|
324 |> Option.map (Lazy.force o snd o snd o fst) |
|
325 |> these; |
|
326 |
|
327 fun continue_history thy = if (#concluded_history o the_spec o the_exec) thy |
|
328 then thy |
|
329 |> (CodeData.map o apfst o map_concluded_history) (K false) |
|
330 |> SOME |
|
331 else NONE; |
|
332 |
|
333 fun conclude_history thy = if (#concluded_history o the_spec o the_exec) thy |
|
334 then NONE |
|
335 else thy |
|
336 |> (CodeData.map o apfst) |
|
337 ((map_eqns o Symtab.map) (fn ((changed, current), history) => |
|
338 ((false, current), |
|
339 if changed then (serial (), current) :: history else history)) |
|
340 #> map_concluded_history (K true)) |
|
341 |> SOME; |
|
342 |
|
343 val _ = Context.>> (Context.map_theory (CodeData.init |
|
344 #> Theory.at_begin continue_history |
|
345 #> Theory.at_end conclude_history)); |
327 |
346 |
328 |
347 |
329 (* access to data dependent on abstract executable content *) |
348 (* access to data dependent on abstract executable content *) |
330 |
349 |
331 fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest); |
350 fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest); |
378 val post = (#post o the_thmproc) exec; |
397 val post = (#post o the_thmproc) exec; |
379 val functrans = (map fst o #functrans o the_thmproc) exec; |
398 val functrans = (map fst o #functrans o the_thmproc) exec; |
380 val eqns = the_eqns exec |
399 val eqns = the_eqns exec |
381 |> Symtab.dest |
400 |> Symtab.dest |
382 |> (map o apfst) (Code_Unit.string_of_const thy) |
401 |> (map o apfst) (Code_Unit.string_of_const thy) |
|
402 |> (map o apsnd) (snd o fst) |
383 |> sort (string_ord o pairself fst); |
403 |> sort (string_ord o pairself fst); |
384 val dtyps = the_dtyps exec |
404 val dtyps = the_dtyps exec |
385 |> Symtab.dest |
405 |> Symtab.dest |
386 |> map (fn (dtco, (vs, cos)) => |
406 |> map (fn (dtco, (_, (vs, cos)) :: _) => |
387 (Syntax.string_of_typ_global thy (Type (dtco, map TFree vs)), cos)) |
407 (Syntax.string_of_typ_global thy (Type (dtco, map TFree vs)), cos)) |
388 |> sort (string_ord o pairself fst) |
408 |> sort (string_ord o pairself fst) |
389 in |
409 in |
390 (Pretty.writeln o Pretty.chunks) [ |
410 (Pretty.writeln o Pretty.chunks) [ |
391 Pretty.block ( |
411 Pretty.block ( |
468 let |
487 let |
469 val base_constraints = Sorts.mg_domain algebra tyco [class]; |
488 val base_constraints = Sorts.mg_domain algebra tyco [class]; |
470 val classparam_constraints = Sorts.complete_sort algebra [class] |
489 val classparam_constraints = Sorts.complete_sort algebra [class] |
471 |> maps (map fst o these o try (#params o AxClass.get_info thy)) |
490 |> maps (map fst o these o try (#params o AxClass.get_info thy)) |
472 |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco)) |
491 |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco)) |
473 |> map (Symtab.lookup ((the_eqns o the_exec) thy)) |
492 |> maps (map fst o get_eqns thy) |
474 |> (map o Option.map) (map fst o Lazy.force o snd) |
|
475 |> maps these |
|
476 |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn); |
493 |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn); |
477 val inter_sorts = map2 (curry (Sorts.inter_sort algebra)); |
494 val inter_sorts = map2 (curry (Sorts.inter_sort algebra)); |
478 in fold inter_sorts classparam_constraints base_constraints end; |
495 in fold inter_sorts classparam_constraints base_constraints end; |
479 |
496 |
480 fun retrieve_algebra thy operational = |
497 fun retrieve_algebra thy operational = |
500 fun delete_force msg key xs = |
517 fun delete_force msg key xs = |
501 if AList.defined (op =) xs key then AList.delete (op =) key xs |
518 if AList.defined (op =) xs key then AList.delete (op =) key xs |
502 else error ("No such " ^ msg ^ ": " ^ quote key); |
519 else error ("No such " ^ msg ^ ": " ^ quote key); |
503 |
520 |
504 fun get_datatype thy tyco = |
521 fun get_datatype thy tyco = |
505 case Symtab.lookup ((the_dtyps o the_exec) thy) tyco |
522 case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) |
506 of SOME spec => spec |
523 of (_, spec) :: _ => spec |
507 | NONE => Sign.arity_number thy tyco |
524 | [] => Sign.arity_number thy tyco |
508 |> Name.invents Name.context Name.aT |
525 |> Name.invents Name.context Name.aT |
509 |> map (rpair []) |
526 |> map (rpair []) |
510 |> rpair []; |
527 |> rpair []; |
511 |
528 |
512 fun get_datatype_of_constr thy c = |
529 fun get_datatype_of_constr thy c = |
513 case (snd o strip_type o Sign.the_const_type thy) c |
530 case (snd o strip_type o Sign.the_const_type thy) c |
514 of Type (tyco, _) => if member (op =) |
531 of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c |
515 ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o the_exec) thy)) tyco) c |
|
516 then SOME tyco else NONE |
532 then SOME tyco else NONE |
517 | _ => NONE; |
533 | _ => NONE; |
518 |
534 |
519 fun get_constr_typ thy c = |
535 fun get_constr_typ thy c = |
520 case get_datatype_of_constr thy c |
536 case get_datatype_of_constr thy c |
523 val SOME tys = AList.lookup (op =) cos c; |
539 val SOME tys = AList.lookup (op =) cos c; |
524 val ty = tys ---> Type (tyco, map TFree vs); |
540 val ty = tys ---> Type (tyco, map TFree vs); |
525 in SOME (Logic.varifyT ty) end |
541 in SOME (Logic.varifyT ty) end |
526 | NONE => NONE; |
542 | NONE => NONE; |
527 |
543 |
528 val get_case_data = Symtab.lookup o fst o the_cases o the_exec; |
544 fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns |
529 |
545 o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), []))) |
530 val is_undefined = Symtab.defined o snd o the_cases o the_exec; |
546 o apfst) (fn (_, eqns) => (true, f eqns)); |
531 |
547 |
532 fun gen_add_eqn linear strict default thm thy = |
548 fun gen_add_eqn linear default thm thy = |
533 case (if strict then SOME o mk_eqn thy linear else mk_liberal_eqn thy) thm |
549 case (if default then mk_default_eqn thy else SOME o mk_eqn thy linear) thm |
534 of SOME (thm, _) => |
550 of SOME (thm, _) => |
535 let |
551 let |
536 val c = Code_Unit.const_eqn thm; |
552 val c = Code_Unit.const_eqn thm; |
537 val _ = if strict andalso (is_some o AxClass.class_of_param thy) c |
553 val _ = if not default andalso (is_some o AxClass.class_of_param thy) c |
538 then error ("Rejected polymorphic equation for overloaded constant:\n" |
554 then error ("Rejected polymorphic equation for overloaded constant:\n" |
539 ^ Display.string_of_thm thm) |
555 ^ Display.string_of_thm thm) |
540 else (); |
556 else (); |
541 val _ = if strict andalso (is_some o get_datatype_of_constr thy) c |
557 val _ = if not default andalso (is_some o get_datatype_of_constr thy) c |
542 then error ("Rejected equation for datatype constructor:\n" |
558 then error ("Rejected equation for datatype constructor:\n" |
543 ^ Display.string_of_thm thm) |
559 ^ Display.string_of_thm thm) |
544 else (); |
560 else (); |
545 in |
561 in change_eqns false c (add_thm thy default (thm, linear)) thy end |
546 (map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default |
|
547 (c, (true, Lazy.value [])) (add_thm thy default (thm, linear))) thy |
|
548 end |
|
549 | NONE => thy; |
562 | NONE => thy; |
550 |
563 |
551 val add_eqn = gen_add_eqn true true false; |
564 val add_eqn = gen_add_eqn true false; |
552 val add_liberal_eqn = gen_add_eqn true false false; |
565 val add_default_eqn = gen_add_eqn true true; |
553 val add_default_eqn = gen_add_eqn true false true; |
566 val add_nonlinear_eqn = gen_add_eqn false false; |
554 val add_nonlinear_eqn = gen_add_eqn false true false; |
|
555 |
|
556 fun del_eqn thm thy = case mk_syntactic_eqn thy thm |
|
557 of SOME (thm, _) => let val c = Code_Unit.const_eqn thm |
|
558 in map_exec_purge (SOME [c]) (map_eqns (Symtab.map_entry c (del_thm thm))) thy end |
|
559 | NONE => thy; |
|
560 |
|
561 fun del_eqns c = map_exec_purge (SOME [c]) |
|
562 (map_eqns (Symtab.map_entry c (K (false, Lazy.value [])))); |
|
563 |
567 |
564 fun add_eqnl (c, lthms) thy = |
568 fun add_eqnl (c, lthms) thy = |
565 let |
569 let |
566 val lthms' = certificate thy |
570 val lthms' = certificate thy |
567 (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms; |
571 (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms; |
568 in |
572 in change_eqns false c (add_lthms lthms') thy end; |
569 map_exec_purge (SOME [c]) |
|
570 (map_eqns (Symtab.map_default (c, (true, Lazy.value [])) |
|
571 (add_lthms lthms'))) thy |
|
572 end; |
|
573 |
573 |
574 val add_default_eqn_attr = Attrib.internal (fn _ => Thm.declaration_attribute |
574 val add_default_eqn_attr = Attrib.internal (fn _ => Thm.declaration_attribute |
575 (fn thm => Context.mapping (add_default_eqn thm) I)); |
575 (fn thm => Context.mapping (add_default_eqn thm) I)); |
|
576 |
|
577 fun del_eqn thm thy = case mk_syntactic_eqn thy thm |
|
578 of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thm) (del_thm thm) thy |
|
579 | NONE => thy; |
|
580 |
|
581 fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); |
|
582 |
|
583 val get_case_data = Symtab.lookup o fst o the_cases o the_exec; |
|
584 |
|
585 val is_undefined = Symtab.defined o snd o the_cases o the_exec; |
576 |
586 |
577 structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); |
587 structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); |
578 |
588 |
579 fun add_datatype raw_cs thy = |
589 fun add_datatype raw_cs thy = |
580 let |
590 let |
581 val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs; |
591 val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs; |
582 val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs; |
592 val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs; |
583 val cs' = map fst (snd vs_cos); |
593 val cs' = map fst (snd vs_cos); |
584 val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco |
594 val purge_cs = case get_datatype thy tyco |
585 of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos) |
595 of (_, []) => NONE |
586 | NONE => NONE; |
596 | (_, cos) => SOME (cs' @ map fst cos); |
587 in |
597 in |
588 thy |
598 thy |
589 |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos)) |
599 |> map_exec_purge purge_cs |
|
600 ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos)) |
590 #> map_eqns (fold (Symtab.delete_safe o fst) cs)) |
601 #> map_eqns (fold (Symtab.delete_safe o fst) cs)) |
591 |> TypeInterpretation.data (tyco, serial ()) |
602 |> TypeInterpretation.data (tyco, serial ()) |
592 end; |
603 end; |
593 |
604 |
594 fun type_interpretation f = TypeInterpretation.interpretation |
605 fun type_interpretation f = TypeInterpretation.interpretation |