lcc/Hcompta/LCC/Sym/Zipper.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Zipper'.
   4 module Hcompta.LCC.Sym.Zipper where
   5
   6 import Control.Applicative (Alternative(..))
   7 import Control.Monad (Monad, liftM, liftM2)
   8 import Data.Eq (Eq)
   9 import Data.Function (($))
  10 import Data.NonNull (NonNull)
  11 import Data.Maybe (Maybe(..))
  12 import Data.Monoid (Monoid(..))
  13 import Data.Ord (Ord)
  14 import Data.Proxy
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Text.Show (Show(..))
  17 import qualified Prelude ()
  18 import qualified Data.TreeMap.Strict.Zipper as Zipper
  19 import qualified Data.TreeMap.Strict as TreeMap
  20 import Data.TreeMap.Strict.Zipper (Zipper)
  21
  22 import Language.Symantic
  23 -- import Language.Symantic.Lib.Lambda
  24 import qualified Language.Symantic.Lib as Sym
  25
  26 -- * Class 'Sym_Zipper'
  27 class Sym_Zipper term where
  28         zipper_descendant         :: Ord k => term (Zipper k a) -> term [Zipper k a]
  29         zipper_descendant_or_self :: Ord k => term (Zipper k a) -> term [Zipper k a]
  30         zipper_child              :: Ord k => term (Zipper k a) -> term [Zipper k a]
  31         zipper_child_lookup       :: (Ord k, Alternative f) => term k -> term (Zipper k a) -> term (f (Zipper k a))
  32         zipper_child_lookups      :: (Ord k, Alternative f, Monad f) => term (TreeMap.Path k) -> term (Zipper k a) -> term (f (Zipper k a))
  33         zipper_child_first        :: (Ord k, Alternative f) => term (Zipper k a) -> term (f (Zipper k a))
  34         zipper_child_last         :: (Ord k, Alternative f) => term (Zipper k a) -> term (f (Zipper k a))
  35         zipper_ancestor           :: Ord k => term (Zipper k a) -> term [Zipper k a]
  36         zipper_ancestor_or_self   :: Ord k => term (Zipper k a) -> term [Zipper k a]
  37         zipper_preceding          :: Ord k => term (Zipper k a) -> term [Zipper k a]
  38         zipper_preceding_sibling  :: Ord k => term (Zipper k a) -> term [Zipper k a]
  39         zipper_following          :: Ord k => term (Zipper k a) -> term [Zipper k a]
  40         zipper_following_sibling  :: Ord k => term (Zipper k a) -> term [Zipper k a]
  41         zipper_parent             :: Ord k => term (Zipper k a) -> term [Zipper k a]
  42         default zipper_descendant         :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  43         default zipper_descendant_or_self :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  44         default zipper_child              :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  45         default zipper_child_lookup       :: (Trans t term, Ord k, Alternative f) => t term k -> t term (Zipper k a) -> t term (f (Zipper k a))
  46         default zipper_child_lookups      :: (Trans t term, Ord k, Alternative f, Monad f) => t term (TreeMap.Path k) -> t term (Zipper k a) -> t term (f (Zipper k a))
  47         default zipper_child_first        :: (Trans t term, Ord k, Alternative f) => t term (Zipper k a) -> t term (f (Zipper k a))
  48         default zipper_child_last         :: (Trans t term, Ord k, Alternative f) => t term (Zipper k a) -> t term (f (Zipper k a))
  49         default zipper_ancestor           :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  50         default zipper_ancestor_or_self   :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  51         default zipper_preceding          :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  52         default zipper_preceding_sibling  :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  53         default zipper_following          :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  54         default zipper_following_sibling  :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  55         default zipper_parent             :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
  56         zipper_descendant         = trans_map1 zipper_descendant
  57         zipper_descendant_or_self = trans_map1 zipper_descendant_or_self
  58         zipper_child              = trans_map1 zipper_child
  59         zipper_child_lookup       = trans_map2 zipper_child_lookup
  60         zipper_child_lookups      = trans_map2 zipper_child_lookups
  61         zipper_child_first        = trans_map1 zipper_child_first
  62         zipper_child_last         = trans_map1 zipper_child_last
  63         zipper_ancestor           = trans_map1 zipper_ancestor
  64         zipper_ancestor_or_self   = trans_map1 zipper_ancestor_or_self
  65         zipper_preceding          = trans_map1 zipper_preceding
  66         zipper_preceding_sibling  = trans_map1 zipper_preceding_sibling
  67         zipper_following          = trans_map1 zipper_preceding
  68         zipper_following_sibling  = trans_map1 zipper_preceding
  69         zipper_parent             = trans_map1 zipper_preceding
  70
  71 type instance Sym_of_Iface (Proxy Zipper) = Sym_Zipper
  72 type instance TyConsts_of_Iface (Proxy Zipper) = Proxy Zipper ': TyConsts_imported_by (Proxy Zipper)
  73 type instance TyConsts_imported_by (Proxy Zipper) =
  74  [ Proxy Eq
  75  , Proxy Show
  76  , Proxy []
  77  ]
  78
  79 instance Sym_Zipper HostI where
  80         zipper_descendant         = liftM  Zipper.zipper_descendant
  81         zipper_descendant_or_self = liftM  Zipper.zipper_descendant_or_self
  82         zipper_child              = liftM  Zipper.zipper_child
  83         zipper_child_lookup       = liftM2 Zipper.zipper_child_lookup
  84         zipper_child_lookups      = liftM2 Zipper.zipper_child_lookups
  85         zipper_child_first        = liftM  Zipper.zipper_child_first
  86         zipper_child_last         = liftM  Zipper.zipper_child_last
  87         zipper_ancestor           = liftM  Zipper.zipper_ancestor
  88         zipper_ancestor_or_self   = liftM  Zipper.zipper_ancestor_or_self
  89         zipper_preceding          = liftM  Zipper.zipper_preceding
  90         zipper_preceding_sibling  = liftM  Zipper.zipper_preceding_sibling
  91         zipper_following          = liftM  Zipper.zipper_following
  92         zipper_following_sibling  = liftM  Zipper.zipper_following_sibling
  93         zipper_parent             = liftM  Zipper.zipper_parent
  94 instance Sym_Zipper TextI where
  95         zipper_descendant         = textI1 "zipper_descendant"
  96         zipper_descendant_or_self = textI1 "zipper_descendant_or_self"
  97         zipper_child              = textI1 "zipper_child"
  98         zipper_child_lookup       = textI2 "zipper_child_lookup"
  99         zipper_child_lookups      = textI2 "zipper_child_lookups"
 100         zipper_child_first        = textI1 "zipper_child_first"
 101         zipper_child_last         = textI1 "zipper_child_last"
 102         zipper_ancestor           = textI1 "zipper_ancestor"
 103         zipper_ancestor_or_self   = textI1 "zipper_ancestor_or_self"
 104         zipper_preceding          = textI1 "zipper_preceding"
 105         zipper_preceding_sibling  = textI1 "zipper_preceding_sibling"
 106         zipper_following          = textI1 "zipper_following"
 107         zipper_following_sibling  = textI1 "zipper_following_sibling"
 108         zipper_parent             = textI1 "zipper_parent"
 109 instance (Sym_Zipper r1, Sym_Zipper r2) => Sym_Zipper (DupI r1 r2) where
 110         zipper_descendant         = dupI1 @Sym_Zipper zipper_descendant
 111         zipper_descendant_or_self = dupI1 @Sym_Zipper zipper_descendant_or_self
 112         zipper_child              = dupI1 @Sym_Zipper zipper_child
 113         zipper_child_lookup       = dupI2 @Sym_Zipper zipper_child_lookup
 114         zipper_child_lookups      = dupI2 @Sym_Zipper zipper_child_lookups
 115         zipper_child_first        = dupI1 @Sym_Zipper zipper_child_first
 116         zipper_child_last         = dupI1 @Sym_Zipper zipper_child_last
 117         zipper_ancestor           = dupI1 @Sym_Zipper zipper_ancestor
 118         zipper_ancestor_or_self   = dupI1 @Sym_Zipper zipper_ancestor_or_self
 119         zipper_preceding          = dupI1 @Sym_Zipper zipper_preceding
 120         zipper_preceding_sibling  = dupI1 @Sym_Zipper zipper_preceding_sibling
 121         zipper_following          = dupI1 @Sym_Zipper zipper_following
 122         zipper_following_sibling  = dupI1 @Sym_Zipper zipper_following_sibling
 123         zipper_parent             = dupI1 @Sym_Zipper zipper_parent
 124
 125 instance
 126  ( Read_TyNameR TyName cs rs
 127  , Inj_TyConst cs Zipper
 128  ) => Read_TyNameR TyName cs (Proxy Zipper ': rs) where
 129         read_TyNameR _cs (TyName "Zipper") k = k (ty @Zipper)
 130         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 131 instance Show_TyConst cs => Show_TyConst (Proxy Zipper ': cs) where
 132         show_TyConst TyConstZ{} = "Zipper"
 133         show_TyConst (TyConstS c) = show_TyConst c
 134
 135 instance Proj_TyFamC cs Sym.TyFam_MonoElement Zipper
 136
 137 instance -- Proj_TyConC
 138  ( Proj_TyConst cs Zipper
 139  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Zipper))
 140  , Proj_TyCon cs
 141  , Inj_TyConst cs Ord
 142  ) => Proj_TyConC cs (Proxy Zipper) where
 143         proj_TyConC _ (TyConst _q :$ (TyConst c :$ _k))
 144          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 145          , Just Refl <- proj_TyConst c (Proxy @Zipper)
 146          = case () of
 147                    {-
 148                  _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
 149                    | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
 150                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
 151                          -}
 152                  _ -> Nothing
 153         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a))
 154          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 155          , Just Refl <- proj_TyConst c (Proxy @Zipper)
 156          = case () of
 157                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)
 158                    , Just TyCon  <- proj_TyCon (t :$ k)
 159                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 160                    {-
 161                    | Just Refl <- proj_TyConst q (Proxy @Ord)
 162                    , Just TyCon  <- proj_TyCon (t :$ k)
 163                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 164                    | Just Refl <- proj_TyConst q (Proxy @Monoid)
 165                    , Just TyCon  <- proj_TyCon (ty @Ord :$ k) -> Just TyCon
 166                    -}
 167                    | Just Refl <- proj_TyConst q (Proxy @Show)
 168                    , Just TyCon  <- proj_TyCon (t :$ k)
 169                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 170                  _ -> Nothing
 171         proj_TyConC _c _q = Nothing
 172 data instance TokenT meta (ts::[*]) (Proxy Zipper)
 173  = Token_Term_Zipper_descendant         (EToken meta ts)
 174  | Token_Term_Zipper_descendant_or_self (EToken meta ts)
 175  | Token_Term_Zipper_child              (EToken meta ts)
 176  | Token_Term_Zipper_child_lookup       (EToken meta '[Proxy Token_Type]) (EToken meta ts) (EToken meta ts)
 177  | Token_Term_Zipper_child_lookups      (EToken meta '[Proxy Token_Type]) (EToken meta ts) (EToken meta ts)
 178  | Token_Term_Zipper_child_first        (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 179  | Token_Term_Zipper_child_last         (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 180  | Token_Term_Zipper_ancestor           (EToken meta ts)
 181  | Token_Term_Zipper_ancestor_or_self   (EToken meta ts)
 182  | Token_Term_Zipper_preceding          (EToken meta ts)
 183  | Token_Term_Zipper_preceding_sibling  (EToken meta ts)
 184  | Token_Term_Zipper_following          (EToken meta ts)
 185  | Token_Term_Zipper_following_sibling  (EToken meta ts)
 186  | Token_Term_Zipper_parent             (EToken meta ts)
 187 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Zipper))
 188 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Zipper))
 189
 190 instance -- CompileI
 191  ( Inj_TyConst cs Zipper
 192  , Inj_TyConst cs []
 193  , Inj_TyConst cs Ord
 194  , Inj_TyConst cs Alternative
 195  , Inj_TyConst cs Monad
 196  , Inj_TyConst cs NonNull
 197  , Proj_TyCon cs
 198  , Read_TyName TyName cs
 199  , Compile cs is
 200  ) => CompileI cs is (Proxy Zipper) where
 201         compileI tok ctx k =
 202                 case tok of
 203                  Token_Term_Zipper_descendant         tok_z -> comp tok_z zipper_descendant
 204                  Token_Term_Zipper_descendant_or_self tok_z -> comp tok_z zipper_descendant_or_self
 205                  Token_Term_Zipper_child              tok_z -> comp tok_z zipper_child
 206                  Token_Term_Zipper_child_lookup  tok_ty_f tok_x tok_z -> comp_lookup  tok_ty_f tok_x tok_z zipper_child_lookup
 207                  Token_Term_Zipper_child_lookups tok_ty_f tok_x tok_z -> comp_lookups tok_ty_f tok_x tok_z zipper_child_lookups
 208                  Token_Term_Zipper_child_first tok_ty_f tok_z -> comp_child tok_ty_f tok_z zipper_child_first
 209                  Token_Term_Zipper_child_last  tok_ty_f tok_z -> comp_child tok_ty_f tok_z zipper_child_last
 210                  Token_Term_Zipper_ancestor           tok_z -> comp tok_z zipper_ancestor
 211                  Token_Term_Zipper_ancestor_or_self   tok_z -> comp tok_z zipper_ancestor_or_self
 212                  Token_Term_Zipper_preceding          tok_z -> comp tok_z zipper_preceding
 213                  Token_Term_Zipper_preceding_sibling  tok_z -> comp tok_z zipper_preceding_sibling
 214                  Token_Term_Zipper_following          tok_z -> comp tok_z zipper_following
 215                  Token_Term_Zipper_following_sibling  tok_z -> comp tok_z zipper_following_sibling
 216                  Token_Term_Zipper_parent             tok_z -> comp tok_z zipper_parent
 217                 where
 218                 comp tok_z
 219                  (op::forall term k a. (Sym_Zipper term, Ord k)
 220                     => term (Zipper k a) -> term [Zipper k a]) =
 221                         compileO tok_z ctx $ \ty_z (TermO z) ->
 222                         check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
 223                         check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
 224                         k (ty @[] :$ ty_z) $ TermO $
 225                          \c -> op (z c)
 226                 comp_child tok_ty_f tok_z
 227                  (op::forall term f k a. (Sym_Zipper term, Ord k, Alternative f)
 228                     => term (Zipper k a) -> term (f (Zipper k a))) =
 229                         compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
 230                         check_Kind
 231                          (At Nothing (SKiType `SKiArrow` SKiType))
 232                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
 233                         check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
 234                         compileO tok_z ctx $ \ty_z (TermO z) ->
 235                         check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
 236                         check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
 237                         k (ty_f :$ ty_z) $ TermO $
 238                          \c -> op (z c)
 239                 comp_lookup tok_ty_f tok_x tok_z
 240                  (op::forall term f k a. (Sym_Zipper term, Ord k, Alternative f)
 241                     => term k -> term (Zipper k a) -> term (f (Zipper k a))) =
 242                         compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
 243                         check_Kind
 244                          (At Nothing (SKiType `SKiArrow` SKiType))
 245                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
 246                         check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
 247                         compileO tok_x ctx $ \ty_x (TermO x) ->
 248                         compileO tok_z ctx $ \ty_z (TermO z) ->
 249                         check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
 250                         check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
 251                         check_TyEq (At (Just tok_x) ty_x) (At (Just tok_z) ty_k) $ \Refl ->
 252                         k (ty_f :$ ty_z) $ TermO $
 253                          \c -> op (x c) (z c)
 254                 comp_lookups tok_ty_f tok_p tok_z
 255                  (op::forall term f k a. (Sym_Zipper term, Ord k, Alternative f, Monad f)
 256                     => term (TreeMap.Path k) -> term (Zipper k a) -> term (f (Zipper k a))) =
 257                         compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
 258                         check_Kind
 259                          (At Nothing (SKiType `SKiArrow` SKiType))
 260                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
 261                         check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
 262                         check_TyCon (At (Just tok_ty_f) (ty @Monad :$ ty_f)) $ \TyCon ->
 263                         compileO tok_p ctx $ \ty_p (TermO p) ->
 264                         compileO tok_z ctx $ \ty_z (TermO z) ->
 265                         check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
 266                         check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
 267                         check_TyEq
 268                          (At (Just tok_z) $ ty @NonNull :$ (ty @[] :$ ty_k))
 269                          (At (Just tok_p) ty_p) $ \Refl ->
 270                         k (ty_f :$ ty_z) $ TermO $
 271                          \c -> op (p c) (z c)
 272 instance -- TokenizeT
 273  Inj_Token meta ts Zipper =>
 274  TokenizeT meta ts (Proxy Zipper) where
 275         tokenizeT _t = mempty
 276          {- tokenizers_infix = tokenizeTMod []
 277                  [ tokenize1 "-" (infixL 6) Token_Term_Subable_add
 278                  ]
 279          -}
 280 instance -- Gram_Term_AtomsT
 281  ( Alt g
 282  , Gram_Rule g
 283  , Gram_Lexer g
 284  , Gram_Meta meta g
 285  , Inj_Token meta ts Zipper
 286  ) => Gram_Term_AtomsT meta ts (Proxy Zipper) g where
 287         {-
 288         gs_term_atomsT _t =
 289          [ rule "term_account" $
 290                 lexeme $ metaG $
 291                 (\a meta -> ProTok $ inj_EToken meta $ Token_Term_Zipper a)
 292                  <$> g_account
 293          ]
 294                 where
 295                 g_account :: CF g Zipper
 296                 g_account =
 297                         Zipper . NonNull.impureNonNull
 298                          <$> some (id <$ char '/' <*> g_account_section)
 299                 g_account_section :: CF g Zipper_Section
 300                 g_account_section =
 301                         Name . Text.pack
 302                          <$> some (choice $ unicat <$> [Unicat_Letter])
 303         -}