src/Doc/Codegen/Adaptation.thy
changeset 82445 bb1f2a03b370
parent 81713 378b9d6c52b2
equal deleted inserted replaced
82444:7a9164068583 82445:bb1f2a03b370
   202     \item[\<open>Code_Target_Nat\<close>] implements type \<^typ>\<open>nat\<close>
   202     \item[\<open>Code_Target_Nat\<close>] implements type \<^typ>\<open>nat\<close>
   203        by \<^typ>\<open>integer\<close> and thus by target-language built-in integers.
   203        by \<^typ>\<open>integer\<close> and thus by target-language built-in integers.
   204        Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated
   204        Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated
   205        by a preprocessor.
   205        by a preprocessor.
   206 
   206 
   207     \item[\<open>Code_Target_Bit_Shifts\<close>] implements bit shifts on \<^typ>\<open>integer\<close>
       
   208        by target-language operations. Combined with \<open>Code_Target_Int\<close>
       
   209        or \<open>Code_Target_Nat\<close>, bit shifts on \<^typ>\<open>int\<close> or \<^type>\<open>nat\<close> can
       
   210        be implemented by target-language operations.
       
   211 
       
   212     \item[\<open>Code_Target_Numeral\<close>] is a convenience theory
   207     \item[\<open>Code_Target_Numeral\<close>] is a convenience theory
   213        containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>-
   208        containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>-
   214 
   209 
   215     \item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language
   210     \item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language
   216        integers, sacrificing pattern patching in exchange for dramatically
   211        integers, sacrificing pattern patching in exchange for dramatically