2076 section \<open>Coercive subtyping\<close> |
2076 section \<open>Coercive subtyping\<close> |
2077 |
2077 |
2078 text \<open> |
2078 text \<open> |
2079 \begin{matharray}{rcl} |
2079 \begin{matharray}{rcl} |
2080 @{attribute_def (HOL) coercion} & : & @{text attribute} \\ |
2080 @{attribute_def (HOL) coercion} & : & @{text attribute} \\ |
|
2081 @{attribute_def (HOL) coercion_delete} & : & @{text attribute} \\ |
2081 @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\ |
2082 @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\ |
2082 @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\ |
2083 @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\ |
|
2084 @{attribute_def (HOL) coercion_args} & : & @{text attribute} \\ |
2083 \end{matharray} |
2085 \end{matharray} |
2084 |
2086 |
2085 Coercive subtyping allows the user to omit explicit type |
2087 Coercive subtyping allows the user to omit explicit type |
2086 conversions, also called \emph{coercions}. Type inference will add |
2088 conversions, also called \emph{coercions}. Type inference will add |
2087 them as necessary when parsing a term. See |
2089 them as necessary when parsing a term. See |
2088 @{cite "traytel-berghofer-nipkow-2011"} for details. |
2090 @{cite "traytel-berghofer-nipkow-2011"} for details. |
2089 |
2091 |
2090 @{rail \<open> |
2092 @{rail \<open> |
2091 @@{attribute (HOL) coercion} (@{syntax term})? |
2093 @@{attribute (HOL) coercion} (@{syntax term}) |
2092 ; |
2094 ; |
2093 @@{attribute (HOL) coercion_map} (@{syntax term})? |
2095 @@{attribute (HOL) coercion_delete} (@{syntax term}) |
|
2096 ; |
|
2097 @@{attribute (HOL) coercion_map} (@{syntax term}) |
|
2098 ; |
|
2099 @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+) |
2094 \<close>} |
2100 \<close>} |
2095 |
2101 |
2096 \begin{description} |
2102 \begin{description} |
2097 |
2103 |
2098 \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new |
2104 \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new |
2100 @{text "\<sigma>\<^sub>2"} are type constructors without arguments. Coercions are |
2106 @{text "\<sigma>\<^sub>2"} are type constructors without arguments. Coercions are |
2101 composed by the inference algorithm if needed. Note that the type |
2107 composed by the inference algorithm if needed. Note that the type |
2102 inference algorithm is complete only if the registered coercions |
2108 inference algorithm is complete only if the registered coercions |
2103 form a lattice. |
2109 form a lattice. |
2104 |
2110 |
|
2111 \item @{attribute (HOL) "coercion_delete"}~@{text "f"} deletes a |
|
2112 preceding declaration (using @{attribute (HOL) "coercion"}) of the |
|
2113 function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} as a coercion. |
|
2114 |
2105 \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a |
2115 \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a |
2106 new map function to lift coercions through type constructors. The |
2116 new map function to lift coercions through type constructors. The |
2107 function @{text "map"} must conform to the following type pattern |
2117 function @{text "map"} must conform to the following type pattern |
2108 |
2118 |
2109 \begin{matharray}{lll} |
2119 \begin{matharray}{lll} |
2113 |
2123 |
2114 where @{text "t"} is a type constructor and @{text "f\<^sub>i"} is of type |
2124 where @{text "t"} is a type constructor and @{text "f\<^sub>i"} is of type |
2115 @{text "\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i"} or @{text "\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i"}. Registering a map function |
2125 @{text "\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i"} or @{text "\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i"}. Registering a map function |
2116 overwrites any existing map function for this particular type |
2126 overwrites any existing map function for this particular type |
2117 constructor. |
2127 constructor. |
|
2128 |
|
2129 \item @{attribute (HOL) "coercion_args"} can be used to disallow |
|
2130 coercions to be inserted in certain positions in a term. For example, |
|
2131 given the constant @{text "c :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2 \<Rightarrow> \<sigma>\<^sub>3 \<Rightarrow> \<sigma>\<^sub>4"} and the list |
|
2132 of policies @{text "- + 0"} as arguments, coercions will not be |
|
2133 inserted in the first argument of @{text "c"} (policy @{text "-"}); |
|
2134 they may be inserted in the second argument (policy @{text "+"}) |
|
2135 even if the constant @{text "c"} itself is in a position where |
|
2136 coercions are disallowed; the third argument inherits the allowance |
|
2137 of coercsion insertion from the position of the constant @{text "c"} |
|
2138 (policy @{text "0"}). The standard usage of policies is the definition |
|
2139 of syntatic constructs (usually extralogical, i.e., processed and |
|
2140 stripped during type inference), that should not be destroyed by the |
|
2141 insertion of coercions (see, for example, the setup for the case syntax |
|
2142 in @{theory Ctr_Sugar}). |
2118 |
2143 |
2119 \item @{attribute (HOL) "coercion_enabled"} enables the coercion |
2144 \item @{attribute (HOL) "coercion_enabled"} enables the coercion |
2120 inference algorithm. |
2145 inference algorithm. |
2121 |
2146 |
2122 \end{description} |
2147 \end{description} |