709 |
709 |
710 (* parse translations *) |
710 (* parse translations *) |
711 |
711 |
712 local |
712 local |
713 |
713 |
714 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = |
714 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) = |
715 if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg) |
715 Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg) |
716 else raise TERM ("gen_field_tr: " ^ mark, [t]) |
716 | field_update_tr t = raise TERM ("field_update_tr", [t]); |
717 | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); |
717 |
718 |
718 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) = |
719 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) = |
719 field_update_tr t :: field_updates_tr u |
720 if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u |
720 | field_updates_tr t = [field_update_tr t]; |
721 else [gen_field_tr mark sfx tm] |
721 |
722 | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm]; |
722 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t |
723 |
|
724 in |
|
725 |
|
726 fun record_update_tr [t, u] = |
|
727 fold (curry op $) |
|
728 (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t |
|
729 | record_update_tr ts = raise TERM ("record_update_tr", ts); |
723 | record_update_tr ts = raise TERM ("record_update_tr", ts); |
730 |
724 |
731 end; |
725 |
732 |
726 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg) |
733 fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) = |
727 | field_tr t = raise TERM ("field_tr", [t]); |
734 if c = mark then (name, arg) |
728 |
735 else raise TERM ("dest_ext_field: " ^ mark, [t]) |
729 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u |
736 | dest_ext_field _ t = raise TERM ("dest_ext_field", [t]); |
730 | fields_tr t = [field_tr t]; |
737 |
731 |
738 fun dest_ext_fields sep mark (trm as (Const (c, _) $ t $ u)) = |
732 fun record_fields_tr more ctxt t = |
739 if c = sep then dest_ext_field mark t :: dest_ext_fields sep mark u |
|
740 else [dest_ext_field mark trm] |
|
741 | dest_ext_fields _ mark t = [dest_ext_field mark t]; |
|
742 |
|
743 fun gen_ext_fields_tr sep mark sfx more ctxt t = |
|
744 let |
733 let |
745 val thy = ProofContext.theory_of ctxt; |
734 val thy = ProofContext.theory_of ctxt; |
746 fun err msg = raise TERM ("error in record input: " ^ msg, [t]); |
735 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]); |
747 |
736 |
748 val fieldargs = dest_ext_fields sep mark t; |
737 fun split_args (field :: fields) ((name, arg) :: fargs) = |
749 fun splitargs (field :: fields) ((name, arg) :: fargs) = |
|
750 if can (unsuffix name) field |
738 if can (unsuffix name) field |
751 then |
739 then |
752 let val (args, rest) = splitargs fields fargs |
740 let val (args, rest) = split_args fields fargs |
753 in (arg :: args, rest) end |
741 in (arg :: args, rest) end |
754 else err ("expecting field " ^ field ^ " but got " ^ name) |
742 else err ("expecting field " ^ field ^ " but got " ^ name) |
755 | splitargs [] (fargs as (_ :: _)) = ([], fargs) |
743 | split_args [] (fargs as (_ :: _)) = ([], fargs) |
756 | splitargs (_ :: _) [] = err "expecting more fields" |
744 | split_args (_ :: _) [] = err "expecting more fields" |
757 | splitargs _ _ = ([], []); |
745 | split_args _ _ = ([], []); |
758 |
746 |
759 fun mk_ext (fargs as (name, _) :: _) = |
747 fun mk_ext (fargs as (name, _) :: _) = |
760 (case get_fieldext thy (Sign.intern_const thy name) of |
748 (case get_fieldext thy (Sign.intern_const thy name) of |
761 SOME (ext, _) => |
749 SOME (ext, _) => |
762 (case get_extfields thy ext of |
750 (case get_extfields thy ext of |
763 SOME flds => |
751 SOME fields => |
764 let |
752 let |
765 val (args, rest) = splitargs (map fst (but_last flds)) fargs; |
753 val (args, rest) = split_args (map fst (but_last fields)) fargs; |
766 val more' = mk_ext rest; |
754 val more' = mk_ext rest; |
767 in list_comb (Syntax.const (suffix sfx ext), args @ [more']) end |
755 in |
|
756 (* FIXME authentic syntax *) |
|
757 list_comb (Syntax.const (suffix extN ext), args @ [more']) |
|
758 end |
768 | NONE => err ("no fields defined for " ^ ext)) |
759 | NONE => err ("no fields defined for " ^ ext)) |
769 | NONE => err (name ^ " is no proper field")) |
760 | NONE => err (name ^ " is no proper field")) |
770 | mk_ext [] = more; |
761 | mk_ext [] = more; |
771 in mk_ext fieldargs end; |
762 in mk_ext (fields_tr t) end; |
772 |
763 |
773 fun gen_ext_type_tr sep mark sfx more ctxt t = |
764 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t |
|
765 | record_tr _ ts = raise TERM ("record_tr", ts); |
|
766 |
|
767 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t |
|
768 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); |
|
769 |
|
770 |
|
771 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) = |
|
772 (name, arg) |
|
773 | field_type_tr t = raise TERM ("field_type_tr", [t]); |
|
774 |
|
775 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) = |
|
776 field_type_tr t :: field_types_tr u |
|
777 | field_types_tr t = [field_type_tr t]; |
|
778 |
|
779 fun record_field_types_tr more ctxt t = |
774 let |
780 let |
775 val thy = ProofContext.theory_of ctxt; |
781 val thy = ProofContext.theory_of ctxt; |
776 fun err msg = raise TERM ("error in record-type input: " ^ msg, [t]); |
782 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]); |
777 |
783 |
778 val fieldargs = dest_ext_fields sep mark t; |
784 fun split_args (field :: fields) ((name, arg) :: fargs) = |
779 fun splitargs (field :: fields) ((name, arg) :: fargs) = |
|
780 if can (unsuffix name) field then |
785 if can (unsuffix name) field then |
781 let val (args, rest) = splitargs fields fargs |
786 let val (args, rest) = split_args fields fargs |
782 in (arg :: args, rest) end |
787 in (arg :: args, rest) end |
783 else err ("expecting field " ^ field ^ " but got " ^ name) |
788 else err ("expecting field " ^ field ^ " but got " ^ name) |
784 | splitargs [] (fargs as (_ :: _)) = ([], fargs) |
789 | split_args [] (fargs as (_ :: _)) = ([], fargs) |
785 | splitargs (_ :: _) [] = err "expecting more fields" |
790 | split_args (_ :: _) [] = err "expecting more fields" |
786 | splitargs _ _ = ([], []); |
791 | split_args _ _ = ([], []); |
787 |
792 |
788 fun mk_ext (fargs as (name, _) :: _) = |
793 fun mk_ext (fargs as (name, _) :: _) = |
789 (case get_fieldext thy (Sign.intern_const thy name) of |
794 (case get_fieldext thy (Sign.intern_const thy name) of |
790 SOME (ext, alphas) => |
795 SOME (ext, alphas) => |
791 (case get_extfields thy ext of |
796 (case get_extfields thy ext of |
792 SOME flds => |
797 SOME fields => |
793 (let |
798 let |
794 val flds' = but_last flds; |
799 val fields' = but_last fields; |
795 val types = map snd flds'; |
800 val types = map snd fields'; |
796 val (args, rest) = splitargs (map fst flds') fargs; |
801 val (args, rest) = split_args (map fst fields') fargs; |
797 val argtypes = map (Sign.certify_typ thy o decode_type thy) args; |
802 val argtypes = map (Sign.certify_typ thy o decode_type thy) args; |
798 val midx = fold Term.maxidx_typ argtypes 0; |
803 val midx = fold Term.maxidx_typ argtypes 0; |
799 val varifyT = varifyT midx; |
804 val varifyT = varifyT midx; |
800 val vartypes = map varifyT types; |
805 val vartypes = map varifyT types; |
801 |
806 |
802 val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty; |
807 val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty |
|
808 handle Type.TYPE_MATCH => err "type is no proper record (extension)"; |
803 val alphas' = |
809 val alphas' = |
804 map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT) |
810 map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT) |
805 (but_last alphas); |
811 (but_last alphas); |
806 |
812 |
807 val more' = mk_ext rest; |
813 val more' = mk_ext rest; |
808 in |
814 in |
809 list_comb (Syntax.const (suffix sfx ext), alphas' @ [more']) |
815 (* FIXME authentic syntax *) |
810 end handle Type.TYPE_MATCH => |
816 list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more']) |
811 raise err "type is no proper record (extension)") |
817 end |
812 | NONE => err ("no fields defined for " ^ ext)) |
818 | NONE => err ("no fields defined for " ^ ext)) |
813 | NONE => err (name ^ " is no proper field")) |
819 | NONE => err (name ^ " is no proper field")) |
814 | mk_ext [] = more; |
820 | mk_ext [] = more; |
815 |
821 in |
816 in mk_ext fieldargs end; |
822 mk_ext (field_types_tr t) |
817 |
823 end; |
818 fun gen_adv_record_tr sep mark sfx unit ctxt [t] = |
824 |
819 gen_ext_fields_tr sep mark sfx unit ctxt t |
825 (* FIXME @{type_syntax} *) |
820 | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); |
826 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t |
821 |
827 | record_type_tr _ ts = raise TERM ("record_type_tr", ts); |
822 fun gen_adv_record_scheme_tr sep mark sfx ctxt [t, more] = |
828 |
823 gen_ext_fields_tr sep mark sfx more ctxt t |
829 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t |
824 | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); |
830 | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts); |
825 |
831 |
826 fun gen_adv_record_type_tr sep mark sfx unit ctxt [t] = |
832 in |
827 gen_ext_type_tr sep mark sfx unit ctxt t |
|
828 | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); |
|
829 |
|
830 fun gen_adv_record_type_scheme_tr sep mark sfx ctxt [t, more] = |
|
831 gen_ext_type_tr sep mark sfx more ctxt t |
|
832 | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); |
|
833 |
|
834 val adv_record_tr = |
|
835 gen_adv_record_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN HOLogic.unit; |
|
836 |
|
837 val adv_record_scheme_tr = |
|
838 gen_adv_record_scheme_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN; |
|
839 |
|
840 val adv_record_type_tr = |
|
841 gen_adv_record_type_tr |
|
842 @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN |
|
843 (Syntax.term_of_typ false (HOLogic.unitT)); |
|
844 |
|
845 val adv_record_type_scheme_tr = |
|
846 gen_adv_record_type_scheme_tr |
|
847 @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN; |
|
848 |
|
849 |
833 |
850 val parse_translation = |
834 val parse_translation = |
851 [(@{syntax_const "_record_update"}, record_update_tr)]; |
835 [(@{syntax_const "_record_update"}, record_update_tr)]; |
852 |
836 |
853 val adv_parse_translation = |
837 val advanced_parse_translation = |
854 [(@{syntax_const "_record"}, adv_record_tr), |
838 [(@{syntax_const "_record"}, record_tr), |
855 (@{syntax_const "_record_scheme"}, adv_record_scheme_tr), |
839 (@{syntax_const "_record_scheme"}, record_scheme_tr), |
856 (@{syntax_const "_record_type"}, adv_record_type_tr), |
840 (@{syntax_const "_record_type"}, record_type_tr), |
857 (@{syntax_const "_record_type_scheme"}, adv_record_type_scheme_tr)]; |
841 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)]; |
|
842 |
|
843 end; |
858 |
844 |
859 |
845 |
860 (* print translations *) |
846 (* print translations *) |
861 |
847 |
862 val print_record_type_abbr = Unsynchronized.ref true; |
848 val print_record_type_abbr = Unsynchronized.ref true; |