312 COVARIANT => (constraint :: cs, tye_idx) |
313 COVARIANT => (constraint :: cs, tye_idx) |
313 | CONTRAVARIANT => (swap constraint :: cs, tye_idx) |
314 | CONTRAVARIANT => (swap constraint :: cs, tye_idx) |
314 | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx |
315 | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx |
315 handle NO_UNIFIER (msg, _) => |
316 handle NO_UNIFIER (msg, _) => |
316 err_list ctxt (gen_msg err |
317 err_list ctxt (gen_msg err |
317 "failed to unify invariant arguments w.r.t. to the known map function") |
318 "failed to unify invariant arguments w.r.t. to the known map function" ^ msg) |
318 (fst tye_idx) Ts) |
319 (fst tye_idx) Ts) |
319 | INVARIANT => (cs, strong_unify ctxt constraint tye_idx |
320 | INVARIANT => (cs, strong_unify ctxt constraint tye_idx |
320 handle NO_UNIFIER (msg, _) => |
321 handle NO_UNIFIER (msg, _) => |
321 error (gen_msg err ("failed to unify invariant arguments" ^ msg)))); |
322 error (gen_msg err ("failed to unify invariant arguments" ^ msg)))); |
322 val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) |
323 val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) |
592 if a = b |
593 if a = b |
593 then Abs (Name.uu, Type (a, []), Bound 0) |
594 then Abs (Name.uu, Type (a, []), Bound 0) |
594 else |
595 else |
595 (case Symreltab.lookup (coes_of ctxt) (a, b) of |
596 (case Symreltab.lookup (coes_of ctxt) (a, b) of |
596 NONE => raise Fail (a ^ " is not a subtype of " ^ b) |
597 NONE => raise Fail (a ^ " is not a subtype of " ^ b) |
597 | SOME co => co) |
598 | SOME (co, _) => co) |
598 | ((Type (a, Ts)), (Type (b, Us))) => |
599 | ((Type (a, Ts)), (Type (b, Us))) => |
599 if a <> b |
600 if a <> b |
600 then raise Fail ("Different constructors: " ^ a ^ " and " ^ b) |
601 then raise Fail ("Different constructors: " ^ a ^ " and " ^ b) |
601 else |
602 else |
602 let |
603 let |
603 fun inst t Ts = |
604 fun inst t Ts = |
604 Term.subst_vars |
605 Term.subst_vars |
605 (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t; |
606 (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t; |
606 fun sub_co (COVARIANT, TU) = SOME (gen_coercion ctxt tye TU) |
607 fun sub_co (COVARIANT, TU) = SOME (gen_coercion ctxt tye TU) |
607 | sub_co (CONTRAVARIANT, TU) = SOME (gen_coercion ctxt tye (swap TU)) |
608 | sub_co (CONTRAVARIANT, TU) = SOME (gen_coercion ctxt tye (swap TU)) |
608 | sub_co (INVARIANT_TO T, _) = NONE; |
609 | sub_co (INVARIANT_TO _, _) = NONE; |
609 fun ts_of [] = [] |
610 fun ts_of [] = [] |
610 | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); |
611 | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); |
611 in |
612 in |
612 (case Symtab.lookup (tmaps_of ctxt) a of |
613 (case Symtab.lookup (tmaps_of ctxt) a of |
613 NONE => raise Fail ("No map function for " ^ a ^ " known") |
614 NONE => raise Fail ("No map function for " ^ a ^ " known") |
726 fun add_type_map raw_t context = |
727 fun add_type_map raw_t context = |
727 let |
728 let |
728 val ctxt = Context.proof_of context; |
729 val ctxt = Context.proof_of context; |
729 val t = singleton (Variable.polymorphic ctxt) raw_t; |
730 val t = singleton (Variable.polymorphic ctxt) raw_t; |
730 |
731 |
731 fun err_str t = "\n\nThe provided function has the type\n" ^ |
732 fun err_str t = "\n\nThe provided function has the type:\n" ^ |
732 Syntax.string_of_typ ctxt (fastype_of t) ^ |
733 Syntax.string_of_typ ctxt (fastype_of t) ^ |
733 "\n\nThe general type signature of a map function is" ^ |
734 "\n\nThe general type signature of a map function is:" ^ |
734 "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^ |
735 "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^ |
735 "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)"; |
736 "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)."; |
736 |
737 |
737 val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) |
738 val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) |
738 handle Empty => error ("Not a proper map function:" ^ err_str t); |
739 handle Empty => error ("Not a proper map function:" ^ err_str t); |
739 |
740 |
740 fun gen_arg_var ([], []) = [] |
741 fun gen_arg_var ([], []) = [] |
764 val res_av = gen_arg_var (fst res); |
765 val res_av = gen_arg_var (fst res); |
765 in |
766 in |
766 map_tmaps (Symtab.update (snd res, (t, res_av))) context |
767 map_tmaps (Symtab.update (snd res, (t, res_av))) context |
767 end; |
768 end; |
768 |
769 |
|
770 fun transitive_coercion tab G (a, b) = |
|
771 let |
|
772 val path = hd (Graph.irreducible_paths G (a, b)); |
|
773 val path' = fst (split_last path) ~~ tl path; |
|
774 val coercions = map (fst o the o Symreltab.lookup tab) path'; |
|
775 in (Abs (Name.uu, Type (a, []), |
|
776 fold (fn t => fn u => t $ u) coercions (Bound 0)), coercions) |
|
777 end; |
|
778 |
769 fun add_coercion raw_t context = |
779 fun add_coercion raw_t context = |
770 let |
780 let |
771 val ctxt = Context.proof_of context; |
781 val ctxt = Context.proof_of context; |
772 val t = singleton (Variable.polymorphic ctxt) raw_t; |
782 val t = singleton (Variable.polymorphic ctxt) raw_t; |
773 |
783 |
774 fun err_coercion () = error ("Bad type for coercion " ^ |
784 fun err_coercion () = error ("Bad type for a coercion:\n" ^ |
775 Syntax.string_of_term ctxt t ^ ":\n" ^ |
785 Syntax.string_of_term ctxt t ^ " :: " ^ |
776 Syntax.string_of_typ ctxt (fastype_of t)); |
786 Syntax.string_of_typ ctxt (fastype_of t)); |
777 |
787 |
778 val (T1, T2) = Term.dest_funT (fastype_of t) |
788 val (T1, T2) = Term.dest_funT (fastype_of t) |
779 handle TYPE _ => err_coercion (); |
789 handle TYPE _ => err_coercion (); |
780 |
790 |
790 |
800 |
791 fun coercion_data_update (tab, G) = |
801 fun coercion_data_update (tab, G) = |
792 let |
802 let |
793 val G' = maybe_new_nodes [a, b] G |
803 val G' = maybe_new_nodes [a, b] G |
794 val G'' = Graph.add_edge_trans_acyclic (a, b) G' |
804 val G'' = Graph.add_edge_trans_acyclic (a, b) G' |
795 handle Graph.CYCLES _ => error (a ^ " is already a subtype of " ^ b ^ |
805 handle Graph.CYCLES _ => error ( |
796 "!\n\nCannot add coercion of type: " ^ a ^ " => " ^ b); |
806 Syntax.string_of_typ ctxt T1 ^ " is already a subtype of " ^ |
|
807 Syntax.string_of_typ ctxt T2 ^ "!\n\nCannot add coercion of type: " ^ |
|
808 Syntax.string_of_typ ctxt (T1 --> T2)); |
797 val new_edges = |
809 val new_edges = |
798 flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y => |
810 flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y => |
799 if Graph.is_edge G' (x, y) then NONE else SOME (x, y)))); |
811 if Graph.is_edge G' (x, y) then NONE else SOME (x, y)))); |
800 val G_and_new = Graph.add_edge (a, b) G'; |
812 val G_and_new = Graph.add_edge (a, b) G'; |
801 |
813 |
802 fun complex_coercion tab G (a, b) = |
|
803 let |
|
804 val path = hd (Graph.irreducible_paths G (a, b)) |
|
805 val path' = fst (split_last path) ~~ tl path |
|
806 in Abs (Name.uu, Type (a, []), |
|
807 fold (fn t => fn u => t $ u) (map (the o Symreltab.lookup tab) path') (Bound 0)) |
|
808 end; |
|
809 |
|
810 val tab' = fold |
814 val tab' = fold |
811 (fn pair => fn tab => Symreltab.update (pair, complex_coercion tab G_and_new pair) tab) |
815 (fn pair => fn tab => |
|
816 Symreltab.update (pair, transitive_coercion tab G_and_new pair) tab) |
812 (filter (fn pair => pair <> (a, b)) new_edges) |
817 (filter (fn pair => pair <> (a, b)) new_edges) |
813 (Symreltab.update ((a, b), t) tab); |
818 (Symreltab.update ((a, b), (t, [])) tab); |
814 in |
819 in |
815 (tab', G'') |
820 (tab', G'') |
816 end; |
821 end; |
817 in |
822 in |
818 map_coes_and_graph coercion_data_update context |
823 map_coes_and_graph coercion_data_update context |
819 end; |
824 end; |
820 |
825 |
|
826 fun delete_coercion raw_t context = |
|
827 let |
|
828 val ctxt = Context.proof_of context; |
|
829 val t = singleton (Variable.polymorphic ctxt) raw_t; |
|
830 |
|
831 fun err_coercion the = error ("Not" ^ |
|
832 (if the then " the defined " else " a ") ^ "coercion:\n" ^ |
|
833 Syntax.string_of_term ctxt t ^ " :: " ^ |
|
834 Syntax.string_of_typ ctxt (fastype_of t)); |
|
835 |
|
836 val (T1, T2) = Term.dest_funT (fastype_of t) |
|
837 handle TYPE _ => err_coercion false; |
|
838 |
|
839 val a = |
|
840 (case T1 of |
|
841 Type (x, []) => x |
|
842 | _ => err_coercion false); |
|
843 |
|
844 val b = |
|
845 (case T2 of |
|
846 Type (x, []) => x |
|
847 | _ => err_coercion false); |
|
848 |
|
849 fun delete_and_insert tab G = |
|
850 let |
|
851 val pairs = |
|
852 Symreltab.fold (fn ((a, b), (_, ts)) => fn pairs => |
|
853 if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)]; |
|
854 fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab); |
|
855 val (G', tab') = fold delete pairs (G, tab); |
|
856 fun reinsert pair (G, xs) = (case (Graph.irreducible_paths G pair) of |
|
857 [] => (G, xs) |
|
858 | _ => (Graph.add_edge pair G, (pair, transitive_coercion tab' G' pair) :: xs)); |
|
859 val (G'', ins) = fold reinsert pairs (G', []); |
|
860 in |
|
861 (fold Symreltab.update ins tab', G'') |
|
862 end |
|
863 |
|
864 fun show_term t = Pretty.block [Syntax.pretty_term ctxt t, |
|
865 Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)] |
|
866 |
|
867 fun coercion_data_update (tab, G) = |
|
868 (case Symreltab.lookup tab (a, b) of |
|
869 NONE => err_coercion false |
|
870 | SOME (t', []) => if t aconv t' |
|
871 then delete_and_insert tab G |
|
872 else err_coercion true |
|
873 | SOME (t', ts) => if t aconv t' |
|
874 then error ("Cannot delete the automatically derived coercion:\n" ^ |
|
875 Syntax.string_of_term ctxt t ^ " :: " ^ |
|
876 Syntax.string_of_typ ctxt (fastype_of t) ^ |
|
877 Pretty.string_of (Pretty.big_list "\n\nDeleting one of the coercions:" |
|
878 (map show_term ts)) ^ |
|
879 "\nwill also remove the transitive coercion.") |
|
880 else err_coercion true); |
|
881 in |
|
882 map_coes_and_graph coercion_data_update context |
|
883 end; |
|
884 |
|
885 fun print_coercions ctxt = |
|
886 let |
|
887 fun show_coercion ((a, b), (t, _)) = Pretty.block [ |
|
888 Syntax.pretty_typ ctxt (Type (a, [])), |
|
889 Pretty.brk 1, Pretty.str "<:", Pretty.brk 1, |
|
890 Syntax.pretty_typ ctxt (Type (b, [])), |
|
891 Pretty.brk 3, Pretty.block [Pretty.str "using", Pretty.brk 1, |
|
892 Pretty.quote (Syntax.pretty_term ctxt t)]]; |
|
893 in |
|
894 Pretty.big_list "Coercions:" (map show_coercion (Symreltab.dest (coes_of ctxt))) |
|
895 |> Pretty.writeln |
|
896 end; |
|
897 |
|
898 fun print_coercion_maps ctxt = |
|
899 let |
|
900 fun show_map (x, (t, _)) = Pretty.block [ |
|
901 Pretty.str x, Pretty.str ":", Pretty.brk 1, |
|
902 Pretty.quote (Syntax.pretty_term ctxt t)]; |
|
903 in |
|
904 Pretty.big_list "Coercion maps:" (map show_map (Symtab.dest (tmaps_of ctxt))) |
|
905 |> Pretty.writeln |
|
906 end; |
|
907 |
821 |
908 |
822 (* theory setup *) |
909 (* theory setup *) |
823 |
910 |
824 val setup = |
911 val setup = |
825 Context.theory_map add_term_check #> |
912 Context.theory_map add_term_check #> |
826 Attrib.setup @{binding coercion} |
913 Attrib.setup @{binding coercion} |
827 (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) |
914 (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) |
828 "declaration of new coercions" #> |
915 "declaration of new coercions" #> |
|
916 Attrib.setup @{binding coercion_delete} |
|
917 (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t)))) |
|
918 "deletion of coercions" #> |
829 Attrib.setup @{binding coercion_map} |
919 Attrib.setup @{binding coercion_map} |
830 (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) |
920 (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) |
831 "declaration of new map functions"; |
921 "declaration of new map functions"; |
832 |
922 |
|
923 |
|
924 (* outer syntax commands *) |
|
925 |
|
926 val _ = |
|
927 Outer_Syntax.improper_command "print_coercions" "print all coercions" Keyword.diag |
|
928 (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of))) |
|
929 val _ = |
|
930 Outer_Syntax.improper_command "print_coercion_maps" "print all coercion maps" Keyword.diag |
|
931 (Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of))) |
|
932 |
833 end; |
933 end; |