restructured for future incorporation of Haskell
authorhaftmann
Wed Jul 18 20:51:20 2018 +0200 (2 months ago)
changeset 6865765ad2bfc19d2
parent 68656 297ca38c7da5
child 68658 16cc1161ad7f
restructured for future incorporation of Haskell
src/HOL/Library/IArray.thy
     1.1 --- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:19 2018 +0200
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:20 2018 +0200
     1.3 @@ -1,17 +1,19 @@
     1.4 +(*  Title:      HOL/Library/IArray.thy
     1.5 +    Author:     Tobias Nipkow, TU Muenchen
     1.6 +*)
     1.7 +
     1.8  section \<open>Immutable Arrays with Code Generation\<close>
     1.9  
    1.10  theory IArray
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -text\<open>Immutable arrays are lists wrapped up in an additional constructor.
    1.15 +subsection \<open>Fundamental operations\<close>
    1.16 +
    1.17 +text \<open>Immutable arrays are lists wrapped up in an additional constructor.
    1.18  There are no update operations. Hence code generation can safely implement
    1.19  this type by efficient target language arrays.  Currently only SML is
    1.20 -provided. Should be extended to other target languages and more operations.
    1.21 -
    1.22 -Note that arrays cannot be printed directly but only by turning them into
    1.23 -lists first. Arrays could be converted back into lists for printing if they
    1.24 -were wrapped up in an additional constructor.\<close>
    1.25 +provided. Could be extended to other target languages and more operations.\<close>
    1.26  
    1.27  context
    1.28  begin
    1.29 @@ -47,15 +49,7 @@
    1.30  end
    1.31  
    1.32  
    1.33 -subsection \<open>Code Generation\<close>
    1.34 -
    1.35 -code_reserved SML Vector
    1.36 -
    1.37 -code_printing
    1.38 -  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
    1.39 -| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
    1.40 -| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
    1.41 -| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
    1.42 +subsection \<open>Generic code equations\<close>
    1.43  
    1.44  lemma [code]:
    1.45    "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
    1.46 @@ -89,56 +83,6 @@
    1.47    "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    1.48    by (cases as, cases bs) (simp add: equal)
    1.49  
    1.50 -context
    1.51 -begin
    1.52 -
    1.53 -qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
    1.54 -  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
    1.55 -
    1.56 -end
    1.57 -
    1.58 -lemma [code]:
    1.59 -  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
    1.60 -  by simp
    1.61 -
    1.62 -code_printing
    1.63 -  constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
    1.64 -
    1.65 -context
    1.66 -begin
    1.67 -
    1.68 -qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
    1.69 -  [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
    1.70 -
    1.71 -end
    1.72 -
    1.73 -lemma [code]:
    1.74 -  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
    1.75 -  by simp
    1.76 -
    1.77 -lemma [code]:
    1.78 -  "as !! n = IArray.sub' (as, integer_of_nat n)"
    1.79 -  by simp
    1.80 -
    1.81 -code_printing
    1.82 -  constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
    1.83 -
    1.84 -context
    1.85 -begin
    1.86 -
    1.87 -qualified definition length' :: "'a iarray \<Rightarrow> integer" where
    1.88 -  [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
    1.89 -
    1.90 -end
    1.91 -
    1.92 -lemma [code]:
    1.93 -  "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
    1.94 -  by simp
    1.95 -
    1.96 -lemma [code]:
    1.97 -  "IArray.length as = nat_of_integer (IArray.length' as)"
    1.98 -  by simp
    1.99 -
   1.100  context term_syntax
   1.101  begin
   1.102  
   1.103 @@ -149,7 +93,59 @@
   1.104  
   1.105  end
   1.106  
   1.107 -code_printing
   1.108 -  constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   1.109 +
   1.110 +subsection \<open>Auxiliary operations for code generation\<close>
   1.111 +
   1.112 +context
   1.113 +begin
   1.114 +
   1.115 +qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
   1.116 +  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
   1.117 +
   1.118 +lemma [code]:
   1.119 +  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
   1.120 +  by simp
   1.121 +
   1.122 +qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   1.123 +  "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
   1.124 +
   1.125 +lemma [code]:
   1.126 +  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
   1.127 +  by simp
   1.128 +
   1.129 +lemma [code]:
   1.130 +  "as !! n = IArray.sub' (as, integer_of_nat n)"
   1.131 +  by simp
   1.132 +
   1.133 +qualified definition length' :: "'a iarray \<Rightarrow> integer" where
   1.134 +  [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
   1.135 +
   1.136 +lemma [code]:
   1.137 +  "IArray.length' (IArray as) = integer_of_nat (List.length as)"
   1.138 +  by simp
   1.139 +
   1.140 +lemma [code]:
   1.141 +  "IArray.length as = nat_of_integer (IArray.length' as)"
   1.142 +  by simp
   1.143  
   1.144  end
   1.145 +
   1.146 +
   1.147 +subsection \<open>Code Generation for SML\<close>
   1.148 +
   1.149 +text \<open>Note that arrays cannot be printed directly but only by turning them into
   1.150 +lists first. Arrays could be converted back into lists for printing if they
   1.151 +were wrapped up in an additional constructor.\<close>
   1.152 +
   1.153 +code_reserved SML Vector
   1.154 +
   1.155 +code_printing
   1.156 +  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
   1.157 +| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
   1.158 +| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
   1.159 +| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
   1.160 +| constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
   1.161 +| constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
   1.162 +| constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   1.163 +
   1.164 +end