rebase from master

au-ts · Dec 8, 2021 · 3d0f3fa · 3d0f3fa
1 parent f20d661
commit 3d0f3fa
Show file tree

Hide file tree

Showing 11 changed files with 112 additions and 110 deletions.
diff --git a/cogent/examples/cpp2022-artefact/README.md b/cogent/examples/cpp2022-artefact/README.md
@@ -7,6 +7,8 @@ Cogent from this [branch](https://github.com/au-ts/cogent/tree/uabsfuns-decl-fix
 
 The work that is being presented are all the files in **loops**, **sum-example** and the file _bilby/adt/WordArray\_Shallow.thy_.
 
+Note that for MacOS users, some of the make files depend on the GNU version of **sed**, i.e. **gsed** on MacOS.
+
 ## Install Isabelle2019
 
 Follow the instructions for installing.

diff --git a/cogent/examples/cpp2022-artefact/loops/build/Generated_ShallowShared.thy b/cogent/examples/cpp2022-artefact/loops/build/Generated_ShallowShared.thy
@@ -51,22 +51,22 @@ type_synonym 'a WordArrayPutP\<^sub>T = "('a WordArray, 32 word, 'a) WordArrayGe
 
 type_synonym ('acc, 'obsv) StepParam\<^sub>T = "('acc, 'obsv) StepParam"
 
-type_synonym ('acc, 'obsv) StopF = "('acc, 'obsv) StepParam \<Rightarrow> bool"
+type_synonym ('acc, 'obsv) StopF = "('acc, 'obsv) StepParam\<^sub>T \<Rightarrow> bool"
 
-type_synonym ('acc, 'obsv) StepF = "('acc, 'obsv) StepParam \<Rightarrow> 'acc"
+type_synonym ('acc, 'obsv) StepF = "('acc, 'obsv) StepParam\<^sub>T \<Rightarrow> 'acc"
 
-type_synonym ('acc, 'obsv) RepParam\<^sub>T = "(64 word, ('acc, 'obsv) StepParam \<Rightarrow> bool, ('acc, 'obsv) StepParam \<Rightarrow> 'acc, 'acc, 'obsv) RepParam"
+type_synonym ('acc, 'obsv) RepParam\<^sub>T = "(64 word, ('acc, 'obsv) StopF, ('acc, 'obsv) StepF, 'acc, 'obsv) RepParam"
 
 type_synonym 'a Opt\<^sub>T = "(unit, 'a) Opt"
 
-consts wordarray_get :: "('a WordArray, 32 word, 'a) WordArrayGetP \<Rightarrow> 'a"
+consts wordarray_get :: "'a WordArrayGetP\<^sub>T \<Rightarrow> 'a"
 
 consts wordarray_length :: "'a WordArray \<Rightarrow> 32 word"
 
-consts wordarray_put :: "('a WordArray, 32 word, 'a) WordArrayGetP \<Rightarrow> 'a WordArray"
+consts wordarray_put :: "'a WordArrayPutP\<^sub>T \<Rightarrow> 'a WordArray"
 
-consts repeat :: "(64 word, ('acc, 'obsv) StepParam \<Rightarrow> bool, ('acc, 'obsv) StepParam \<Rightarrow> 'acc, 'acc, 'obsv) RepParam \<Rightarrow> 'acc"
+consts repeat :: "('acc, 'obsv) RepParam\<^sub>T \<Rightarrow> 'acc"
 
-consts wordarray_get_opt :: "('a WordArray, 32 word) WordArrayGetOP \<Rightarrow> (unit, 'a) Opt"
+consts wordarray_get_opt :: "'a WordArrayGetOP\<^sub>T \<Rightarrow> 'a Opt\<^sub>T"
 
 end
diff --git a/cogent/examples/cpp2022-artefact/loops/build/Generated_ShallowShared_Tuples.thy b/cogent/examples/cpp2022-artefact/loops/build/Generated_ShallowShared_Tuples.thy
@@ -42,22 +42,22 @@ type_synonym 'a WordArrayPutP\<^sub>T = "('a WordArray, 32 word, 'a) WordArrayGe
 
 type_synonym ('acc, 'obsv) StepParam\<^sub>T = "('acc, 'obsv) StepParam"
 
-type_synonym ('acc, 'obsv) StopF = "('acc, 'obsv) StepParam \<Rightarrow> bool"
+type_synonym ('acc, 'obsv) StopF = "('acc, 'obsv) StepParam\<^sub>T \<Rightarrow> bool"
 
-type_synonym ('acc, 'obsv) StepF = "('acc, 'obsv) StepParam \<Rightarrow> 'acc"
+type_synonym ('acc, 'obsv) StepF = "('acc, 'obsv) StepParam\<^sub>T \<Rightarrow> 'acc"
 
-type_synonym ('acc, 'obsv) RepParam\<^sub>T = "(64 word, ('acc, 'obsv) StepParam \<Rightarrow> bool, ('acc, 'obsv) StepParam \<Rightarrow> 'acc, 'acc, 'obsv) RepParam"
+type_synonym ('acc, 'obsv) RepParam\<^sub>T = "(64 word, ('acc, 'obsv) StopF, ('acc, 'obsv) StepF, 'acc, 'obsv) RepParam"
 
 type_synonym 'a Opt\<^sub>T = "(unit, 'a) Opt"
 
-consts wordarray_get :: "('a WordArray, 32 word, 'a) WordArrayGetP \<Rightarrow> 'a"
+consts wordarray_get :: "'a WordArrayGetP\<^sub>T \<Rightarrow> 'a"
 
 consts wordarray_length :: "'a WordArray \<Rightarrow> 32 word"
 
-consts wordarray_put :: "('a WordArray, 32 word, 'a) WordArrayGetP \<Rightarrow> 'a WordArray"
+consts wordarray_put :: "'a WordArrayPutP\<^sub>T \<Rightarrow> 'a WordArray"
 
-consts repeat :: "(64 word, ('acc, 'obsv) StepParam \<Rightarrow> bool, ('acc, 'obsv) StepParam \<Rightarrow> 'acc, 'acc, 'obsv) RepParam \<Rightarrow> 'acc"
+consts repeat :: "('acc, 'obsv) RepParam\<^sub>T \<Rightarrow> 'acc"
 
-consts wordarray_get_opt :: "('a WordArray, 32 word) WordArrayGetOP \<Rightarrow> (unit, 'a) Opt"
+consts wordarray_get_opt :: "'a WordArrayGetOP\<^sub>T \<Rightarrow> 'a Opt\<^sub>T"
 
 end
diff --git a/cogent/examples/cpp2022-artefact/loops/build/Generated_Shallow_Desugar.thy b/cogent/examples/cpp2022-artefact/loops/build/Generated_Shallow_Desugar.thy
@@ -8,58 +8,58 @@ imports "Generated_ShallowShared"
 begin
 
 definition
-  wordarray_put32 :: "(32 word WordArray, 32 word, 32 word) WordArrayGetP \<Rightarrow> 32 word WordArray"
+  wordarray_put32 :: "32 word WordArrayPutP\<^sub>T \<Rightarrow> 32 word WordArray"
 where
-  "wordarray_put32 ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>args. (wordarray_put :: (32 word WordArray, 32 word, 32 word) WordArrayGetP \<Rightarrow> 32 word WordArray) args)"
+  "wordarray_put32 ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>args. (wordarray_put :: 32 word WordArrayPutP\<^sub>T \<Rightarrow> 32 word WordArray) args)"
 
 definition
-  expstop :: "(32 word, 32 word) StepParam \<Rightarrow> bool"
+  expstop :: "(32 word, 32 word) StepParam\<^sub>T \<Rightarrow> bool"
 where
   "expstop ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>x. False)"
 
 definition
-  log2stop :: "((64 word, 64 word) T1, 64 word) StepParam \<Rightarrow> bool"
+  log2stop :: "((64 word, 64 word) T1, 64 word) StepParam\<^sub>T \<Rightarrow> bool"
 where
   "log2stop ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 StepParam.acc\<^sub>f) (\<lambda>(acc,ds\<^sub>2). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>2 StepParam.obsv\<^sub>f) (\<lambda>(obsv,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t acc T1.p1\<^sub>f) (\<lambda>(a,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T1.p2\<^sub>f) (\<lambda>(b,ds\<^sub>4). (>=) a obsv))))"
 
 definition
-  searchStop :: "((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) StepParam \<Rightarrow> bool"
+  searchStop :: "((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) StepParam\<^sub>T \<Rightarrow> bool"
 where
   "searchStop ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 StepParam.acc\<^sub>f) (\<lambda>(acc,ds\<^sub>2). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>2 StepParam.obsv\<^sub>f) (\<lambda>(obsv,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t acc T0.p1\<^sub>f) (\<lambda>(l,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T0.p2\<^sub>f) (\<lambda>(r,ds\<^sub>4). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>4 T0.p3\<^sub>f) (\<lambda>(b,ds\<^sub>5). HOL.If b True (HOL.If ((>=) l r) True False))))))"
 
 definition
-  expstep :: "(32 word, 32 word) StepParam \<Rightarrow> 32 word"
+  expstep :: "(32 word, 32 word) StepParam\<^sub>T \<Rightarrow> 32 word"
 where
   "expstep ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 StepParam.acc\<^sub>f) (\<lambda>(acc,ds\<^sub>2). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>2 StepParam.obsv\<^sub>f) (\<lambda>(obsv,ds\<^sub>1). (*) acc obsv))"
 
 definition
-  log2step :: "((64 word, 64 word) T1, 64 word) StepParam \<Rightarrow> (64 word, 64 word) T1"
+  log2step :: "((64 word, 64 word) T1, 64 word) StepParam\<^sub>T \<Rightarrow> (64 word, 64 word) T1"
 where
   "log2step ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 StepParam.acc\<^sub>f) (\<lambda>(acc,ds\<^sub>2). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>2 StepParam.obsv\<^sub>f) (\<lambda>(obsv,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t acc T1.p1\<^sub>f) (\<lambda>(a,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T1.p2\<^sub>f) (\<lambda>(b,ds\<^sub>4). T1.make ((*) a (2 :: 64 word)) ((+) b (1 :: 64 word))))))"
 
 definition
-  searchNext :: "((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) StepParam \<Rightarrow> (32 word, 32 word, bool) T0"
+  searchNext :: "((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) StepParam\<^sub>T \<Rightarrow> (32 word, 32 word, bool) T0"
 where
-  "searchNext ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 StepParam.acc\<^sub>f) (\<lambda>(acc,ds\<^sub>2). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>2 StepParam.obsv\<^sub>f) (\<lambda>(obsv,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t acc T0.p1\<^sub>f) (\<lambda>(l,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T0.p2\<^sub>f) (\<lambda>(r,ds\<^sub>4). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>4 T0.p3\<^sub>f) (\<lambda>(b,ds\<^sub>5). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t obsv T1.p1\<^sub>f) (\<lambda>(arr,ds\<^sub>6). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>6 T1.p2\<^sub>f) (\<lambda>(v,ds\<^sub>7). HOL.Let ((+) l (checked_div ((-) r l) (2 :: 32 word))) (\<lambda>m. HOL.Let (WordArrayGetP.make arr m (0 :: 32 word)) (\<lambda>args. HOL.Let ((wordarray_get :: (32 word WordArray, 32 word, 32 word) WordArrayGetP \<Rightarrow> 32 word) args) (\<lambda>x. HOL.If ((<) x v) (T0.make ((+) m (1 :: 32 word)) r b) (HOL.If ((>) x v) (T0.make l m b) (T0.make m r True))))))))))))"
+  "searchNext ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 StepParam.acc\<^sub>f) (\<lambda>(acc,ds\<^sub>2). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>2 StepParam.obsv\<^sub>f) (\<lambda>(obsv,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t acc T0.p1\<^sub>f) (\<lambda>(l,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T0.p2\<^sub>f) (\<lambda>(r,ds\<^sub>4). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>4 T0.p3\<^sub>f) (\<lambda>(b,ds\<^sub>5). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t obsv T1.p1\<^sub>f) (\<lambda>(arr,ds\<^sub>6). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>6 T1.p2\<^sub>f) (\<lambda>(v,ds\<^sub>7). HOL.Let ((+) l (checked_div ((-) r l) (2 :: 32 word))) (\<lambda>m. HOL.Let (WordArrayGetP.make arr m (0 :: 32 word)) (\<lambda>args. HOL.Let ((wordarray_get :: 32 word WordArrayGetP\<^sub>T \<Rightarrow> 32 word) args) (\<lambda>x. HOL.If ((<) x v) (T0.make ((+) m (1 :: 32 word)) r b) (HOL.If ((>) x v) (T0.make l m b) (T0.make m r True))))))))))))"
 
 definition
   binarySearch :: "(32 word WordArray, 32 word) T1 \<Rightarrow> 32 word"
 where
-  "binarySearch ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 T1.p1\<^sub>f) (\<lambda>(arr,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>1 T1.p2\<^sub>f) (\<lambda>(v,ds\<^sub>2). HOL.Let ((wordarray_length :: 32 word WordArray \<Rightarrow> 32 word) arr) (\<lambda>len. HOL.Let (RepParam.make (ucast len :: 64 word) searchStop searchNext (T0.make (0 :: 32 word) len False) (T1.make arr v)) (\<lambda>args. HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ((repeat :: (64 word, ((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) StepParam \<Rightarrow> bool, ((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) StepParam \<Rightarrow> (32 word, 32 word, bool) T0, (32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) RepParam \<Rightarrow> (32 word, 32 word, bool) T0) args) T0.p1\<^sub>f) (\<lambda>(l,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T0.p2\<^sub>f) (\<lambda>(r,ds\<^sub>4). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>4 T0.p3\<^sub>f) (\<lambda>(b,ds\<^sub>5). HOL.If b l len)))))))"
+  "binarySearch ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 T1.p1\<^sub>f) (\<lambda>(arr,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>1 T1.p2\<^sub>f) (\<lambda>(v,ds\<^sub>2). HOL.Let ((wordarray_length :: 32 word WordArray \<Rightarrow> 32 word) arr) (\<lambda>len. HOL.Let (RepParam.make (ucast len :: 64 word) searchStop searchNext (T0.make (0 :: 32 word) len False) (T1.make arr v)) (\<lambda>args. HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ((repeat :: ((32 word, 32 word, bool) T0, (32 word WordArray, 32 word) T1) RepParam\<^sub>T \<Rightarrow> (32 word, 32 word, bool) T0) args) T0.p1\<^sub>f) (\<lambda>(l,ds\<^sub>3). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>3 T0.p2\<^sub>f) (\<lambda>(r,ds\<^sub>4). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>4 T0.p3\<^sub>f) (\<lambda>(b,ds\<^sub>5). HOL.If b l len)))))))"
 
 definition
   myexp :: "(32 word, 32 word) T1 \<Rightarrow> 32 word"
 where
-  "myexp ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 T1.p1\<^sub>f) (\<lambda>(a,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>1 T1.p2\<^sub>f) (\<lambda>(b,ds\<^sub>2). HOL.Let (RepParam.make (ucast b :: 64 word) expstop expstep (1 :: 32 word) a) (\<lambda>args. (repeat :: (64 word, (32 word, 32 word) StepParam \<Rightarrow> bool, (32 word, 32 word) StepParam \<Rightarrow> 32 word, 32 word, 32 word) RepParam \<Rightarrow> 32 word) args)))"
+  "myexp ds\<^sub>0 \<equiv> HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>0 T1.p1\<^sub>f) (\<lambda>(a,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>1 T1.p2\<^sub>f) (\<lambda>(b,ds\<^sub>2). HOL.Let (RepParam.make (ucast b :: 64 word) expstop expstep (1 :: 32 word) a) (\<lambda>args. (repeat :: (32 word, 32 word) RepParam\<^sub>T \<Rightarrow> 32 word) args)))"
 
 definition
   mylog2 :: "64 word \<Rightarrow> 64 word"
 where
-  "mylog2 ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>n. HOL.Let (RepParam.make n log2stop log2step (T1.make (1 :: 64 word) (0 :: 64 word)) n) (\<lambda>args. HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ((repeat :: (64 word, ((64 word, 64 word) T1, 64 word) StepParam \<Rightarrow> bool, ((64 word, 64 word) T1, 64 word) StepParam \<Rightarrow> (64 word, 64 word) T1, (64 word, 64 word) T1, 64 word) RepParam \<Rightarrow> (64 word, 64 word) T1) args) T1.p1\<^sub>f) (\<lambda>(a,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>1 T1.p2\<^sub>f) (\<lambda>(b,ds\<^sub>2). b))))"
+  "mylog2 ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>n. HOL.Let (RepParam.make n log2stop log2step (T1.make (1 :: 64 word) (0 :: 64 word)) n) (\<lambda>args. HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ((repeat :: ((64 word, 64 word) T1, 64 word) RepParam\<^sub>T \<Rightarrow> (64 word, 64 word) T1) args) T1.p1\<^sub>f) (\<lambda>(a,ds\<^sub>1). HOL.Let (take\<^sub>c\<^sub>o\<^sub>g\<^sub>e\<^sub>n\<^sub>t ds\<^sub>1 T1.p2\<^sub>f) (\<lambda>(b,ds\<^sub>2). b))))"
 
 definition
-  wordarray_get_opt32 :: "(32 word WordArray, 32 word) WordArrayGetOP \<Rightarrow> (unit, 32 word) Opt"
+  wordarray_get_opt32 :: "32 word WordArrayGetOP\<^sub>T \<Rightarrow> 32 word Opt\<^sub>T"
 where
-  "wordarray_get_opt32 ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>args. (wordarray_get_opt :: (32 word WordArray, 32 word) WordArrayGetOP \<Rightarrow> (unit, 32 word) Opt) args)"
+  "wordarray_get_opt32 ds\<^sub>0 \<equiv> HOL.Let ds\<^sub>0 (\<lambda>args. (wordarray_get_opt :: 32 word WordArrayGetOP\<^sub>T \<Rightarrow> 32 word Opt\<^sub>T) args)"
 
 end