Fix stack clean.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / List.hs

diff --git a/symantic-lib/Language/Symantic/Lib/List.hs b/symantic-lib/Language/Symantic/Lib/List.hs
index 4ac4ea0aaf19841c304ddee4dd1a8af2b9af58a4..05fa682057ace14cd753a2bed97b6aa6f4eaf041 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/List.hs
+++ b/symantic-lib/Language/Symantic/Lib/List.hs
@@ -27,7 +27,7 @@ import Language.Symantic.Lib.Lambda
 class Sym_List term where
        list_empty     :: term [a]
        list_singleton :: term a -> term [a]
-       (.:)           :: term a -> term [a] -> term [a]
+       (.:)           :: term a -> term [a] -> term [a]; infixr 5 .:
        list           :: [term a] -> term [a]
        zipWith        :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
        
@@ -43,8 +43,6 @@ class Sym_List term where
        list l         = trans_lift (list (trans_apply Functor.<$> l))
        zipWith        = trans_map3 zipWith
 
-infixr 5 .:
-
 type instance Sym_of_Iface (Proxy []) = Sym_List
 type instance TyConsts_of_Iface (Proxy []) = Proxy [] ': TyConsts_imported_by []
 type instance TyConsts_imported_by [] =
@@ -76,15 +74,15 @@ instance Sym_List TextI where
                where op = (infixN0, L)
        zipWith = textI3 "zipWith"
 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
-       list_empty = dupI0 (Proxy @Sym_List) list_empty
-       list_singleton = dupI1 (Proxy @Sym_List) list_singleton
-       (.:) = dupI2 (Proxy @Sym_List) (.:)
+       list_empty     = dupI0 @Sym_List list_empty
+       list_singleton = dupI1 @Sym_List list_singleton
+       (.:)           = dupI2 @Sym_List (.:)
        list l =
                let (l1, l2) =
                        Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
                                (x1:xs1, x2:xs2)) ([], []) l in
                list l1 `DupI` list l2
-       zipWith = dupI3 (Proxy @Sym_List) zipWith
+       zipWith = dupI3 @Sym_List zipWith
 
 instance
  ( Read_TyNameR TyName cs rs
@@ -136,20 +134,20 @@ data instance TokenT meta (ts::[*]) (Proxy [])
 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
 instance -- CompileI
- ( Read_TyName TyName (TyConsts_of_Ifaces is)
- , Inj_TyConst (TyConsts_of_Ifaces is) []
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Compile is
- ) => CompileI is (Proxy []) where
+ ( Read_TyName TyName cs
+ , Inj_TyConst        cs []
+ , Inj_TyConst        cs (->)
+ , Compile cs is
+ ) => CompileI cs is (Proxy []) where
        compileI
         :: forall meta ctx ret ls rs.
         TokenT meta is (Proxy [])
-        -> CompileT meta ctx ret is ls (Proxy [] ': rs)
+        -> CompileT meta ctx ret cs is ls (Proxy [] ': rs)
        compileI tok ctx k =
                case tok of
                 Token_Term_List_empty tok_ty_a ->
                        -- [] :: [a]
-                       compile_Type tok_ty_a $ \(ty_a::Type (TyConsts_of_Ifaces is) a) ->
+                       compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
                        check_Kind
                         (At Nothing SKiType)
                         (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
@@ -171,16 +169,16 @@ instance -- CompileI
                        k ty_as $ TermO $
                         \c -> a c .: as c
                 Token_Term_List_list tok_ty_a tok_as ->
-                       compile_Type tok_ty_a $ \(ty_a::Type (TyConsts_of_Ifaces is) a) ->
+                       compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
                        check_Kind
                         (At Nothing SKiType)
                         (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
                        go (At (Just tok_ty_a) ty_a) [] tok_as
                        where
-                       go :: At meta '[Proxy Token_Type] (Type (TyConsts_of_Ifaces is) ty_a)
+                       go :: At meta '[Proxy Token_Type] (Type cs ty_a)
                           -> [TermO ctx ty_a is '[] is]
                           -> [EToken meta is]
-                          -> Either (Error_Term meta is) ret
+                          -> Either (Error_Term meta cs is) ret
                        go ty_a as [] =
                                k (ty @[] :$ unAt ty_a) $ TermO $
                                 \c -> list $ (\(TermO a) -> a c)
@@ -203,10 +201,10 @@ instance -- TokenizeT
  TokenizeT meta ts (Proxy []) where
        tokenizeT _t = mempty
         { tokenizers_infix = tokenizeTMod []
-                [ (Term_Name "[]",) $ Term_ProTok
-                        { term_protok = \meta -> ProTokPi $ \a ->
+                [ (TeName "[]",) $ ProTok_Term
+                        { protok_term = \meta -> ProTokPi $ \a ->
                                ProTok $ inj_EToken meta $ Token_Term_List_empty a
-                        , term_fixity = infixN5
+                        , protok_fixity = infixN5
                         }
                 , tokenize2 ":" (infixR 5) Token_Term_List_cons
                 , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
@@ -220,7 +218,7 @@ instance
  , Inj_Token meta ts (->)
  , Inj_Token meta ts []
  ) => Gram_Term_AtomsT meta ts (Proxy []) g where
-       term_atomsT _t =
+       gs_term_atomsT _t =
         [ rule "term_list" $
                ProTok <$> between (symbol "[") (symbol "]") listG
         , rule "term_list_empty" $
@@ -236,5 +234,5 @@ instance
                        (\a mb meta -> inj_EToken meta $ case mb of
                         Just b  -> Token_Term_List_cons a b
                         Nothing -> Token_Term_List_singleton a)
-                        <$> termG
+                        <$> g_term
                         <*> option Nothing (Just <$ symbol "," <*> listG)