Update saw-core tuple syntax in heapster-saw/examples.

GaloisInc · Mar 18, 2022 · 454b0da · 454b0da
1 parent aec37ef
commit 454b0da
Show file tree

Hide file tree

Showing 13 changed files with 91 additions and 82 deletions.
diff --git a/heapster-saw/examples/arrays.sawcore b/heapster-saw/examples/arrays.sawcore
@@ -3,39 +3,48 @@ module arrays where
 
 import Prelude;
 
+letRecM_single :
+  (lrt : LetRecType) ->
+  (B : sort 0) ->
+  (lrtToType lrt -> lrtToType lrt) ->
+  (lrtToType lrt -> CompM B) -> CompM B;
+letRecM_single lrt B fn body =
+  letRecM
+    (LRT_Cons lrt LRT_Nil) B
+    (\ (x : lrtToType lrt) -> consTuple (lrtToType lrt) TypeNil (fn x) ())
+    (\ (x : lrtToType lrt) -> body x);
+
 -- The helper function for noErrorsContains0
 --
 -- noErrorsContains0H len i v =
 --   orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
 noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-                     CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+                     CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
 noErrorsContains0H len_top i_top v_top =
-  letRecM
-    (LRT_Cons
-     (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
-      LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
-      LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
-      LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
-     LRT_Nil)
-    (BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
+  letRecM_single
+    (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
+     LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
+     LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
+     LRT_Ret #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))))
+    #(BVVec 64 len_top (Vec 64 Bool), Vec 64 Bool)
     (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
-       ((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
-           precondHint
-             (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
-             (and (bvsle 64 0x0000000000000000 i)
-                  (bvsle 64 i 0x0fffffffffffffff))
-             (orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                  (existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                           (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                           (returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
-                  (f len (bvAdd 64 i 0x0000000000000001) v))), ()))
+            CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
+       (\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
+          precondHint
+            (CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool))
+            (and (bvsle 64 0x0000000000000000 i)
+                 (bvsle 64 i 0x0fffffffffffffff))
+            (orM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
+                 (existsM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
+                          #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
+                          (returnM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))
+                 (f len (bvAdd 64 i 0x0000000000000001) v))))
     (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+            CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
        f len_top i_top v_top);
 
 -- The specification that contains0 has no errors
 noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-                    CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+                    CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
 noErrorsContains0 len v =
   noErrorsContains0H len 0x0000000000000000 v;
diff --git a/heapster-saw/examples/clearbufs.sawcore b/heapster-saw/examples/clearbufs.sawcore
@@ -25,28 +25,28 @@ Mbox_def = Mbox;
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
 
---unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool));
+--unfoldMbox : Mbox -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool));
 primitive
-unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool)));
+unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> #(Mbox, BVVec 64 len (Vec 64 Bool))));
 
 {-unfoldMbox m =
-  Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()))
-  (Left #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) ())
-  (\ (m:Mbox) (_:Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #())) (len:Vec 64 Bool) (d:BVVec 64 bv64_16 (Vec 64 Bool)) ->
-     Right #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) (m, len, d, ()))
+  Mbox__rec (\ (_:Mbox) -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()))
+  (Left #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) ())
+  (\ (m:Mbox) (_:Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #())) (len:Vec 64 Bool) (d:BVVec 64 bv64_16 (Vec 64 Bool)) ->
+     Right #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) (m, len, d, ()))
   m;
   -}
 
 primitive
-foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool))) -> Mbox;
+foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> #(Mbox, BVVec 64 len (Vec 64 Bool)))) -> Mbox;
 
---(Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) -> Mbox;
+--#(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #()) -> Mbox;
 {-
 foldMbox =
-  either #() (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) Mbox
+  either #() #(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #()) Mbox
          (\ (_:#()) -> Mbox_nil)
-         (\ (tup : (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #())) ->
-            Mbox_cons tup.1 tup.2 tup.3);
+         (\ (tup : #(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #())) ->
+            Mbox_cons tup.0 tup.1 tup.2);
 			-}
 
 primitive

diff --git a/heapster-saw/examples/global_var.sawcore b/heapster-saw/examples/global_var.sawcore
@@ -2,8 +2,8 @@ module GlobalVar where
 
 import Prelude;
 
-acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
-acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
+acquireLockM : Vec 64 Bool -> CompM #(Vec 64 Bool, Vec 64 Bool);
+acquireLockM u = returnM #(Vec 64 Bool, Vec 64 Bool)
 			 (u,u);
 
 releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);

diff --git a/heapster-saw/examples/iter_linked_list.sawcore b/heapster-saw/examples/iter_linked_list.sawcore
@@ -27,20 +27,20 @@ ListF__rec : (a b:sort 0) -> (P : ListF a b -> sort 0) ->
              (l:ListF a b) -> P l;
 ListF__rec a b P f1 f2 l = ListF#rec a b P f1 f2 l;
 
-unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b);
+unfoldListF : (a b:sort 0) -> ListF a b -> Either b #(a, ListF a b);
 unfoldListF a b l =
-  ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b))
-  (\ (x:b) -> Left b (a * ListF a b) x)
-  (\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b)) ->
-     Right b (a * ListF a b) (x, l))
+  ListF__rec a b (\ (_:ListF a b) -> Either b #(a, ListF a b))
+  (\ (x:b) -> Left b #(a, ListF a b) x)
+  (\ (x:a) (l:ListF a b) (_:Either b #(a, ListF a b)) ->
+     Right b #(a, ListF a b) (x, l))
   l;
 
-foldListF : (a b:sort 0) -> Either b (a * ListF a b) -> ListF a b;
+foldListF : (a b:sort 0) -> Either b #(a, ListF a b) -> ListF a b;
 foldListF a b =
-  either b (a * ListF a b) (ListF a b)
+  either b #(a, ListF a b) (ListF a b)
          (\ (x : b) -> NilF a b x)
-         (\ (tup : (a * ListF a b)) ->
-            ConsF a b tup.(1) tup.(2));
+         (\ (tup : #(a, ListF a b)) ->
+            ConsF a b tup.0 tup.1);
 
 getListF : (a b:sort 0) -> ListF a b -> b;
 getListF a b =

diff --git a/heapster-saw/examples/mbox.saw b/heapster-saw/examples/mbox.saw
@@ -73,7 +73,7 @@ heapster_assume_fun env "__memcpy_chk"
   "(len:bv 64). arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword (len)) -o \
               \ arg0:byte_array<W,len>, arg1:byte_array<W,len>"
   "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> \
-    \ returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
+    \ returnM #(BVVec 64 len (Vec 8 Bool), BVVec 64 len (Vec 8 Bool)) (src, src)";
 
 
 //------------------------------------------------------------------------------

diff --git a/heapster-saw/examples/mbox.sawcore b/heapster-saw/examples/mbox.sawcore
@@ -31,20 +31,20 @@ Mbox__rec : (P : Mbox -> sort 0) ->
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m;
 
-unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool));
+unfoldMbox : Mbox -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool));
 unfoldMbox m =
-  Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)))
-  (Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) ())
-  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
-     Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
+  Mbox__rec (\ (_:Mbox) -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)))
+  (Left #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) ())
+  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
+     Right #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
   m;
 
-foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
+foldMbox : Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
 foldMbox =
-  either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
+  either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
          (\ (_:#()) -> Mbox_nil)
-         (\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) ->
-            Mbox_cons tup.1 tup.2 tup.3 tup.(2).(2).(2));
+         (\ (tup : #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) ->
+            Mbox_cons tup.0 tup.1 tup.2 tup.3);
 
 {-
 getMbox : (a : sort 0) -> Mbox a -> a;

diff --git a/heapster-saw/examples/memcpy.saw b/heapster-saw/examples/memcpy.saw
@@ -10,7 +10,7 @@ heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
   \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
   \ arg2:eq(llvmword(len)) -o \
   \ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
-  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
+  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM #(#(), #()) ((),())";
 
 
 heapster_typecheck_fun env "copy_int"

diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw
@@ -105,7 +105,7 @@ heapster_define_opaque_llvmshape env "Vec" 64
 // Opaque type for HashMap<T,U>
 heapster_define_opaque_llvmshape env "HashMap" 64
   "T:llvmshape 64, U:llvmshape 64" "56"
-  "\\ (T:sort 0) (U:sort 0) -> List (T * U)";
+  "\\ (T:sort 0) (U:sort 0) -> List #(T, U)";
 
 // BinTree<X> type
 heapster_define_rust_type env
@@ -234,7 +234,7 @@ heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc"
 heapster_assume_fun env "llvm.uadd.with.overflow.i64"
   "(). arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)"
   "\\ (x y:Vec 64 Bool) -> \
-    \ returnM (Vec 64 Bool * Vec 1 Bool) (bvAdd 64 x y, single Bool (bvCarry 64 x y))";
+    \ returnM #(Vec 64 Bool, Vec 1 Bool) (bvAdd 64 x y, single Bool (bvCarry 64 x y))";
 
 // llvm.expect.i1
 heapster_assume_fun env "llvm.expect.i1"
@@ -248,7 +248,7 @@ heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
   \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
   \ arg2:eq(llvmword(len)) -o \
   \ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
-  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
+  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM #(#(), #()) ((),())";
 
 // Box<List20<u64>>::clone
 box_list20_u64_clone_sym <- heapster_find_symbol_with_type env

diff --git a/heapster-saw/examples/rust_data.sawcore b/heapster-saw/examples/rust_data.sawcore
@@ -3,17 +3,17 @@ module rust_data where
 
 import Prelude;
 
-unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
+unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
 unfoldListPermH a l =
-  List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
-  (Left #() (#() * a * List a) ())
-  (\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
-     Right #() (#() * a * List a) ((), x, l))
+  List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
+  (Left #() #(#(), a, List a) ())
+  (\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
+     Right #() #(#(), a, List a) ((), x, l))
   l;
 
-foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
+foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
 foldListPermH a =
-  either #() (#() * a * List a) (List a)
+  either #() #(#(), a, List a) (List a)
          (\ (_ : #()) -> Nil a)
-         (\ (tup : (#() * a * List a)) ->
-            Cons a tup.(2).(1) tup.(2).(2));
+         (\ (tup : #(#(), a, List a)) ->
+            Cons a tup.1 tup.2);
diff --git a/heapster-saw/examples/rust_lifetimes.saw b/heapster-saw/examples/rust_lifetimes.saw
@@ -26,7 +26,7 @@ heapster_assume_fun env "llvm.uadd.with.overflow.i64"
   "(). arg0:int64<>, arg1:int64<> -o \
      \ ret:struct(int64<>,int1<>)"
   "\\ (x y:Vec 64 Bool) -> \
-    \ returnM (Vec 64 Bool * Vec 1 Bool) \
+    \ returnM #(Vec 64 Bool, Vec 1 Bool) \
     \         (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y))";
 
 // llvm.expect.i1

diff --git a/heapster-saw/examples/rust_lifetimes.sawcore b/heapster-saw/examples/rust_lifetimes.sawcore
@@ -3,17 +3,17 @@ module rust_lifetimes where
 
 import Prelude;
 
-unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
+unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
 unfoldListPermH a l =
-  List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
-  (Left #() (#() * a * List a) ())
-  (\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
-     Right #() (#() * a * List a) ((), x, l))
+  List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
+  (Left #() #(#(), a, List a) ())
+  (\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
+     Right #() #(#(), a, List a) ((), x, l))
   l;
 
-foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
+foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
 foldListPermH a =
-  either #() (#() * a * List a) (List a)
+  either #() #(#(), a, List a) (List a)
          (\ (_ : #()) -> Nil a)
-         (\ (tup : (#() * a * List a)) ->
-            Cons a tup.(2).(1) tup.(2).(2));
+         (\ (tup : #(#(), a, List a)) ->
+            Cons a tup.1 tup.2);
diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw
@@ -10,7 +10,7 @@ heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
 heapster_assume_fun env "CRYPTO_load_u64_be"
   "(). arg0:ptr((R,0) |-> int64<>) -o \
      \ arg0:ptr((R,0) |-> int64<>), ret:int64<>"
-  "\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x, x)";
+  "\\ (x:Vec 64 Bool) -> returnM #(Vec 64 Bool, Vec 64 Bool) (x, x)";
 
 heapster_typecheck_fun env "return_state"
   "(). arg0:array(W,0,<8,*8,fieldsh(int64<>)) -o \

diff --git a/heapster-saw/examples/string_set.sawcore b/heapster-saw/examples/string_set.sawcore
@@ -8,10 +8,10 @@ listInsertM a l s =
   returnM (List a) (Cons a s l);
 
 listRemoveM : (a : sort 0) -> (a -> a -> Bool) -> List a -> a ->
-              CompM (List a * a);
+              CompM #(List a, a);
 listRemoveM a test_eq l s =
   returnM
-    (List a * a)
+    #(List a, a)
     (List__rec
       a (\ (_:List a) -> List a)
       (Nil a)
@@ -30,10 +30,10 @@ stringListInsertM : List String -> String -> CompM (List String);
 stringListInsertM l s =
   returnM (List String) (Cons String s l);
 
-stringListRemoveM : List String -> String -> CompM (stringList * String);
+stringListRemoveM : List String -> String -> CompM #(stringList, String);
 stringListRemoveM l s =
   returnM
-    (stringList * String)
+    #(stringList, String)
     (List__rec
       String (\ (_:List String) -> List String)
       (Nil String)