Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorlammich <lammich@in.tum.de>
Fri, 02 Jun 2017 09:26:04 +0200
changeset 66005 10e5265c2a25
parent 66004 797ef4889177 (diff)
parent 66002 c85f677cfb0a (current diff)
child 66006 cec184536dfd
merged
--- a/src/HOL/Imperative_HOL/Array.thy	Thu Jun 01 23:22:40 2017 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jun 02 09:26:04 2017 +0200
@@ -443,14 +443,14 @@
 
 code_printing type_constructor array \<rightharpoonup> (SML) "_/ array"
 code_printing constant Array \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Array\")"
-code_printing constant Array.new' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))"
+code_printing constant Array.new' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.array/ (IntInf.toInt _,/ (_)))"
 code_printing constant Array.of_list \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.fromList/ _)"
-code_printing constant Array.make' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))"
-code_printing constant Array.len' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.length/ _)"
-code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))"
-code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))"
+code_printing constant Array.make' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.tabulate/ (IntInf.toInt _,/ _ o IntInf.fromInt))"
+code_printing constant Array.len' \<rightharpoonup> (SML) "(fn/ ()/ =>/ IntInf.fromInt (Array.length/ _))"
+code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ IntInf.toInt _))"
+code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ IntInf.toInt _,/ (_)))"
 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
-
+  
 code_reserved SML Array
 
 
--- a/src/HOL/Imperative_HOL/Heap.thy	Thu Jun 01 23:22:40 2017 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Jun 02 09:26:04 2017 +0200
@@ -32,6 +32,8 @@
 
 instance String.literal :: heap ..
 
+instance char :: heap ..
+
 instance typerep :: heap ..
 
 
@@ -76,6 +78,10 @@
 instance ref :: (type) countable
   by (rule countable_classI [of addr_of_ref]) simp
 
+instance array :: (type) heap ..
+instance ref :: (type) heap ..
+    
+    
 text \<open>Syntactic convenience\<close>
 
 setup \<open>
isabelle