Agda module parametrization

plutus-metatheory/src/MAlonzo/Code/Utils.hs

@@ -622,3 +622,78 @@ cover_Kind_652 x
       Star -> ()
       Sharp -> ()
       Arrow _ _ -> ()
+-- Utils.M.f
+d_f_670 :: () -> AgdaAny -> AgdaAny
+d_f_670 ~v0 v1 = du_f_670 v1
+du_f_670 :: AgdaAny -> AgdaAny
+du_f_670 v0 = coe v0
+-- Utils.MNat.f
+d_f_676 :: Integer -> Integer
+d_f_676 v0 = coe v0
+-- Utils.testM
+d_testM_680 :: () -> AgdaAny -> AgdaAny
+d_testM_680 ~v0 v1 = du_testM_680 v1
+du_testM_680 :: AgdaAny -> AgdaAny
+du_testM_680 v0 = coe v0
+-- Utils.ByteString'
+d_ByteString''_682 = ()
+data T_ByteString''_682
+  = C_mkBS_708 AgdaAny (AgdaAny -> AgdaAny -> AgdaAny)
+               (T_List_384 AgdaAny -> AgdaAny) (AgdaAny -> T_List_384 AgdaAny)
+-- Utils.ByteString'.W8
+d_W8_696 :: T_ByteString''_682 -> ()
+d_W8_696 = erased
+-- Utils.ByteString'.BS
+d_BS_698 :: T_ByteString''_682 -> ()
+d_BS_698 = erased
+-- Utils.ByteString'.empty
+d_empty_700 :: T_ByteString''_682 -> AgdaAny
+d_empty_700 v0
+  = case coe v0 of
+      C_mkBS_708 v3 v4 v5 v6 -> coe v3
+      _ -> MAlonzo.RTE.mazUnreachableError
+-- Utils.ByteString'.cons
+d_cons_702 :: T_ByteString''_682 -> AgdaAny -> AgdaAny -> AgdaAny
+d_cons_702 v0
+  = case coe v0 of
+      C_mkBS_708 v3 v4 v5 v6 -> coe v4
+      _ -> MAlonzo.RTE.mazUnreachableError
+-- Utils.ByteString'.pack
+d_pack_704 :: T_ByteString''_682 -> T_List_384 AgdaAny -> AgdaAny
+d_pack_704 v0
+  = case coe v0 of
+      C_mkBS_708 v3 v4 v5 v6 -> coe v5
+      _ -> MAlonzo.RTE.mazUnreachableError
+-- Utils.ByteString'.unpack
+d_unpack_706 :: T_ByteString''_682 -> AgdaAny -> T_List_384 AgdaAny
+d_unpack_706 v0
+  = case coe v0 of
+      C_mkBS_708 v3 v4 v5 v6 -> coe v6
+      _ -> MAlonzo.RTE.mazUnreachableError
+-- Utils.b
+d_b_710 :: T_ByteString''_682
+d_b_710
+  = coe
+      C_mkBS_708 (coe C_'91''93'_388) (coe C__'8759'__390) (\ v0 -> v0)
+      (\ v0 -> v0)
+-- Utils.AST1._.BS
+d_BS_722 :: T_ByteString''_682 -> ()
+d_BS_722 = erased
+-- Utils.AST1._.W8
+d_W8_724 :: T_ByteString''_682 -> ()
+d_W8_724 = erased
+-- Utils.AST1._.cons
+d_cons_726 :: T_ByteString''_682 -> AgdaAny -> AgdaAny -> AgdaAny
+d_cons_726 v0 = coe d_cons_702 (coe v0)
+-- Utils.AST1._.empty
+d_empty_728 :: T_ByteString''_682 -> AgdaAny
+d_empty_728 v0 = coe d_empty_700 (coe v0)
+-- Utils.AST1._.pack
+d_pack_730 :: T_ByteString''_682 -> T_List_384 AgdaAny -> AgdaAny
+d_pack_730 v0 = coe d_pack_704 (coe v0)
+-- Utils.AST1._.unpack
+d_unpack_732 :: T_ByteString''_682 -> AgdaAny -> T_List_384 AgdaAny
+d_unpack_732 v0 = coe d_unpack_706 (coe v0)
+-- Utils.AST1.x
+d_x_734 :: T_ByteString''_682 -> AgdaAny
+d_x_734 v0 = coe d_empty_700 (coe v0)

plutus-metatheory/src/Utils.lagda.md

@@ -375,3 +375,39 @@ Let `I`, `J`, `K` range over kinds:
 variable
   I J K : Kind
 ```
+
+```
+module M (A : Set) where
+
+  f : A → A
+  f x = x 
+
+module MNat = M ℕ
+
+
+-- testM : ℕ
+testM : (A : Set) → A → A
+testM = M.f
+
+record ByteString' : Set₁ where
+  constructor mkBS
+  field
+    W8 : Set
+    BS : Set
+    empty : BS
+    cons : W8 → BS → BS
+    pack : List W8 → BS
+    unpack : BS → List W8
+
+b : ByteString' 
+b = record { W8 = ℕ ; BS = List ℕ ; empty = [] ; cons = _∷_ ; pack = λ z → z ; unpack = λ z → z } 
+
+module AST1 (b' : ByteString') where
+
+  open ByteString' b'
+
+  x : BS
+  x = empty
+
+
+```