equal
deleted
inserted
replaced
419 |
419 |
420 |
420 |
421 |
421 |
422 (** record field splitting **) |
422 (** record field splitting **) |
423 |
423 |
|
424 (* tactic *) |
|
425 |
424 fun record_split_tac i st = |
426 fun record_split_tac i st = |
425 let |
427 let |
426 val (_, (sps, ss)) = RecordsData.get_sg (Thm.sign_of_thm st); |
428 val (_, (sps, ss)) = RecordsData.get_sg (Thm.sign_of_thm st); |
427 |
429 |
428 fun is_fieldT (_, Type (a, [_, _])) = is_some (Symtab.lookup (sps, a)) |
430 fun is_fieldT (_, Type (a, [_, _])) = is_some (Symtab.lookup (sps, a)) |
431 in |
433 in |
432 if exists is_fieldT params then Simplifier.full_simp_tac ss i st |
434 if exists is_fieldT params then Simplifier.full_simp_tac ss i st |
433 else Seq.empty |
435 else Seq.empty |
434 end handle Library.LIST _ => Seq.empty; |
436 end handle Library.LIST _ => Seq.empty; |
435 |
437 |
|
438 |
|
439 (* wrapper *) |
|
440 |
436 val record_split_name = "record_split_tac"; |
441 val record_split_name = "record_split_tac"; |
437 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac); |
442 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac); |
|
443 |
|
444 |
|
445 (* method *) |
|
446 |
|
447 val record_split_method = |
|
448 ("record_split", Method.no_args (Method.METHOD0 (FIRSTGOAL record_split_tac)), |
|
449 "split record fields"); |
438 |
450 |
439 |
451 |
440 |
452 |
441 (** internal theory extenders **) |
453 (** internal theory extenders **) |
442 |
454 |
856 val add_record = gen_add_record read_typ read_raw_parent; |
868 val add_record = gen_add_record read_typ read_raw_parent; |
857 val add_record_i = gen_add_record cert_typ (K I); |
869 val add_record_i = gen_add_record cert_typ (K I); |
858 |
870 |
859 |
871 |
860 |
872 |
861 (** setup theory **) |
873 (** package setup **) |
|
874 |
|
875 (* setup theory *) |
862 |
876 |
863 val setup = |
877 val setup = |
864 [RecordsData.init, |
878 [RecordsData.init, |
865 Theory.add_trfuns ([], parse_translation, [], []), |
879 Theory.add_trfuns ([], parse_translation, [], []), |
|
880 Method.add_methods [record_split_method], |
866 add_wrapper record_split_wrapper]; |
881 add_wrapper record_split_wrapper]; |
867 |
882 |
|
883 |
|
884 (* outer syntax *) |
|
885 |
|
886 open OuterParse; |
|
887 |
|
888 val record_decl = |
|
889 type_args -- name -- ($$$ "=" |-- Scan.option (typ --| $$$ "+") |
|
890 -- Scan.repeat1 (name -- ($$$ "::" |-- typ))); |
|
891 |
|
892 val recordP = |
|
893 OuterSyntax.parser false "record" "define extensible record" |
|
894 (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); |
|
895 |
|
896 val _ = OuterSyntax.add_parsers [recordP]; |
868 |
897 |
869 end; |
898 end; |
870 |
899 |
871 |
900 |
872 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage; |
901 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage; |