Language/Symantic/Expr/From.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE GADTs #-}
   6 {-# LANGUAGE KindSignatures #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Expr.From where
  14
  15 import Data.Maybe (fromMaybe)
  16 import Data.Proxy (Proxy(..))
  17 import Data.Text (Text)
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import GHC.Prim (Constraint)
  20
  21 import Language.Symantic.Type
  22 import Language.Symantic.Expr.Root
  23 import Language.Symantic.Expr.Alt
  24 import Language.Symantic.Expr.Error
  25
  26 -- * Class 'Expr_from'
  27 -- | Parse given @ast@ into
  28 -- a 'Type_Root_of_Expr' and
  29 -- a 'Forall_Repr_with_Context',
  30 -- or return an 'Error_of_Expr'.
  31 class Expr_from ast (ex:: *) where
  32         expr_from :: Expr_From ast ex hs ret
  33 instance -- Expr_from
  34  ( Expr_from ast (ex (Expr_Root ex))
  35  , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
  36  ) => Expr_from ast (Expr_Root ex) where
  37         expr_from _ex ctx ast k =
  38                 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
  39                  ctx ast $ \ty (Forall_Repr_with_Context repr) ->
  40                         k ty (Forall_Repr_with_Context repr)
  41 instance -- Expr_from
  42  ( Expr_from ast (curr root)
  43  , Expr_from ast (next root)
  44  , Root_of_Expr (curr root) ~ root
  45  , Root_of_Expr (next root) ~ root
  46  , Unlift_Error_Expr (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
  47                                  (Type_Root_of_Expr root) ast)
  48                      (Error_of_Expr ast root)
  49  ) => Expr_from ast (Expr_Alt curr next root) where
  50         expr_from _ex ctx ast k =
  51                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
  52                  \ty (Forall_Repr_with_Context repr) ->
  53                         Right $ k ty (Forall_Repr_with_Context repr) of
  54                  Right ret -> ret
  55                  Left err ->
  56                         case unlift_error_expr err of
  57                          Just (Error_Expr_Unsupported_here _
  58                           :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
  59                                         (Type_Root_of_Expr root) ast) ->
  60                                 expr_from (Proxy::Proxy (next root)) ctx ast $
  61                                  \ty (Forall_Repr_with_Context repr) ->
  62                                 k ty (Forall_Repr_with_Context repr)
  63                          _ -> Left err
  64
  65 -- ** Type 'Expr_From'
  66 type Expr_From ast ex hs ret
  67  = Proxy ex
  68  -- ^ Select the 'Expr_from' instance.
  69  -> ast
  70  -- ^ The input data to parse.
  71  -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
  72  -- ^ The bound variables in scope and their types:
  73  -- held in the heterogeneous list @hs@,
  74  -- from the closest including lambda abstraction to the farest.
  75  -> ( forall h
  76     .  Type_Root_of_Expr ex h
  77     -> Forall_Repr_with_Context ex hs h
  78     -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
  79  -- ^ The accumulating continuation.
  80  ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
  81
  82 -- ** Type 'Context'
  83 -- | GADT for a typing context,
  84 -- accumulating an @item@ at each lambda;
  85 -- used to accumulate object-types (in 'Expr_from')
  86 -- or host-terms (in 'Repr_Host')
  87 -- associated with the 'Lambda_Var's in scope.
  88 data Context :: (* -> *) -> [*] -> * where
  89         Context_Empty :: Context item '[]
  90         Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
  91 infixr 5 `Context_Next`
  92
  93 -- ** Type 'Lambda_Var'
  94 -- | Join a name and a type.
  95 --
  96 -- This data type is used to handle lambda variables by name
  97 -- (instead of DeBruijn indices for instance).
  98 data Lambda_Var ty h
  99  =   Lambda_Var Lambda_Var_Name (ty h)
 100 type Lambda_Var_Name = Text
 101
 102 -- ** Type 'Forall_Repr_with_Context'
 103 -- | A data type embedding a universal quantification
 104 -- over an interpreter @repr@
 105 -- and qualified by the symantics of an expression.
 106 --
 107 -- Moreover the expression is abstracted by a 'Context'
 108 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
 109 -- for lambda abstractions.
 110 --
 111 -- This data type is used to keep a parsed expression polymorphic enough
 112 -- to stay interpretable by different interpreters.
 113 --
 114 -- NOTE: 'Sym_of_Expr'@ ex repr@
 115 -- is needed to be able to use symantic methods of the parsed expression
 116 -- into a 'Forall_Repr_with_Context'@ ex@.
 117 --
 118 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
 119 -- is needed to be able to use an expression
 120 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
 121 -- into a 'Forall_Repr_with_Context'@ ex@,
 122 -- which happens when a symantic method includes a polymorphic type
 123 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
 124 data Forall_Repr_with_Context ex hs h
 125  =   Forall_Repr_with_Context
 126  (   forall repr. ( Sym_of_Expr ex repr
 127                   , Sym_of_Expr (Root_of_Expr ex) repr
 128                   ) => Context repr hs -> repr h )
 129
 130 -- ** Type 'Forall_Repr'
 131 data Forall_Repr ex h
 132  =   Forall_Repr
 133  { unForall_Repr :: forall repr
 134                  .  ( Sym_of_Expr ex repr
 135                     , Sym_of_Expr (Root_of_Expr ex) repr )
 136                  => repr h }
 137
 138 -- ** Type family 'Sym_of_Expr'
 139 -- | The symantic of an expression.
 140 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
 141 type instance Sym_of_Expr (Expr_Root ex) repr
 142  =            Sym_of_Expr (ex (Expr_Root ex)) repr
 143 type instance Sym_of_Expr (Expr_Alt curr next root) repr
 144  = ( Sym_of_Expr (curr root) repr
 145    , Sym_of_Expr (next root) repr
 146    )
 147
 148 -- * Checks
 149
 150 -- | Parsing utility to check that two types are equal,
 151 -- or raise 'Error_Expr_Type_mismatch'.
 152 check_TypeFamily
 153  :: forall ast ex ta root ty h ret.
 154  ( root ~ Root_of_Expr ex
 155  , ty ~ Type_Root_of_Expr ex
 156  , TypeFamily ta ty
 157  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 158                    (Error_of_Expr ast root)
 159  ) => Proxy ta -> Proxy ex -> ast -> ty h
 160  -> (ty (Host_of_TypeFamily ta h) -> Either (Error_of_Expr ast root) ret)
 161  -> Either (Error_of_Expr ast root) ret
 162 check_TypeFamily ta ex ast ty k =
 163         case typeFamily ta ty of
 164          Just t -> k t
 165          Nothing -> Left $ error_expr ex $
 166                 Error_Expr_Type (lift_error_type $ Error_Type_No_TypeFamily ast) ast
 167
 168 -- | Parsing utility to check that two types are equal,
 169 -- or raise 'Error_Expr_Type_mismatch'.
 170 check_eq_type
 171  :: forall ast ex root ty x y ret.
 172  ( root ~ Root_of_Expr ex
 173  , ty ~ Type_Root_of_Expr ex
 174  , Eq_Type ty
 175  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 176                    (Error_of_Expr ast root)
 177  ) => Proxy ex -> ast -> ty x -> ty y
 178  -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 179  -> Either (Error_of_Expr ast root) ret
 180 check_eq_type ex ast x y k =
 181         case x `eq_type` y of
 182          Just Refl -> k Refl
 183          Nothing -> Left $ error_expr ex $
 184                 Error_Expr_Type_mismatch ast
 185                  (Exists_Type x)
 186                  (Exists_Type y)
 187
 188 -- | Parsing utility to check that two 'Type_Type1' are equal,
 189 -- or raise 'Error_Expr_Type_mismatch'.
 190 check_eq_type1
 191  :: forall ast ex root ty h1 h2 a1 a2 ret.
 192  ( root ~ Root_of_Expr ex
 193  , ty ~ Type_Root_of_Expr ex
 194  , Eq_Type1 ty
 195  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 196                    (Error_of_Expr ast root)
 197  )
 198  => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
 199  -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
 200  -> Either (Error_of_Expr ast root) ret
 201 check_eq_type1 ex ast h1 h2 k =
 202         case h1 `eq_type1` h2 of
 203          Just Refl -> k Refl
 204          Nothing -> Left $ error_expr ex $
 205                 Error_Expr_Type_mismatch ast
 206                  (Exists_Type h1)
 207                  (Exists_Type h2)
 208
 209 -- | Parsing utility to check that a 'Type_Type0' or higher
 210 -- is an instance of a given 'Constraint',
 211 -- or raise 'Error_Expr_Constraint_missing'.
 212 check_constraint_type
 213  :: forall ast ex c root ty h ret.
 214  ( root ~ Root_of_Expr ex
 215  , ty ~ Type_Root_of_Expr ex
 216  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 217                    (Error_of_Expr ast root)
 218  , Constraint_Type c ty
 219  )
 220  => Proxy ex -> Proxy c -> ast -> ty h
 221  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 222  -> Either (Error_of_Expr ast root) ret
 223 check_constraint_type ex c ast ty k =
 224         case constraint_type c ty of
 225          Just Dict -> k Dict
 226          Nothing -> Left $ error_expr ex $
 227                 Error_Expr_Constraint_missing ast
 228                  {-(Exists_Dict c)-}
 229                  -- FIXME: not easy to report the constraint
 230                  -- and still support 'Eq' and 'Show' deriving.
 231                  (Exists_Type ty)
 232
 233 -- | Parsing utility to check that a 'Type_Type1' or higher
 234 -- is an instance of a given 'Constraint',
 235 -- or raise 'Error_Expr_Constraint_missing'.
 236 check_constraint_type1
 237  :: forall ast ex c root ty h a ret.
 238  ( root ~ Root_of_Expr ex
 239  , ty ~ Type_Root_of_Expr ex
 240  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 241                    (Error_of_Expr ast root)
 242  , Constraint_Type1 c ty
 243  ) => Proxy ex -> Proxy c -> ast -> ty (h a)
 244  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 245  -> Either (Error_of_Expr ast root) ret
 246 check_constraint_type1 ex c ast ty k =
 247         case constraint_type1 c ty of
 248          Just Dict -> k Dict
 249          Nothing -> Left $ error_expr ex $
 250                 Error_Expr_Constraint_missing ast
 251                  (Exists_Type ty)
 252
 253 -- | Parsing utility to check that the given type is at least a 'Type_Type1'
 254 -- or raise 'Error_Expr_Type_mismatch'.
 255 check_type1
 256  :: forall ast ex root ty h ret.
 257  ( root ~ Root_of_Expr ex
 258  , ty ~ Type_Root_of_Expr ex
 259  , Unlift_Type1 (Type_of_Expr root)
 260  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 261                    (Error_of_Expr ast root)
 262  ) => Proxy ex -> ast -> ty h
 263  -> (forall (t1:: *).
 264      ( Type_Type1 t1 ty h
 265      , Lift_Type1 t1 ty (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
 266      ) -> Either (Error_of_Expr ast root) ret)
 267  -> Either (Error_of_Expr ast root) ret
 268 check_type1 ex ast ty k =
 269         (`fromMaybe` unlift_type1 (unType_Root ty) (Just . k)) $
 270         Left $
 271                 error_expr ex $
 272                 Error_Expr_Type_mismatch ast
 273                  (Exists_Type (type_var1 SZero (type_var0 SZero)
 274                  :: ty (Var1 Var0)))
 275                  (Exists_Type ty)
 276
 277 -- * Parsers
 278
 279 -- | Like 'expr_from' but for a root expression.
 280 root_expr_from
 281  :: forall ast root.
 282  ( Expr_from ast root
 283  , Root_of_Expr root ~ root
 284  ) => Proxy root -> ast
 285  -> Either (Error_of_Expr ast root)
 286            (Exists_Type_and_Repr (Type_Root_of_Expr root)
 287                                  (Forall_Repr root))
 288 root_expr_from _ex ast =
 289         expr_from (Proxy::Proxy root) ast
 290          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
 291                 Right $ Exists_Type_and_Repr ty $
 292                         Forall_Repr $ repr Context_Empty
 293
 294 -- | Parse a literal.
 295 lit_from
 296  :: forall ty lit ex ast hs ret.
 297  ( ty ~ Type_Root_of_Expr ex
 298  , Read lit
 299  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 300                    (Error_of_Expr ast (Root_of_Expr ex))
 301  ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
 302  -> ty lit -> Lambda_Var_Name
 303  -> Expr_From ast ex hs ret
 304 lit_from lit ty_lit toread ex ast _ctx k =
 305         case read_safe toread of
 306          Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
 307          Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
 308
 309 -- | Parse a unary class operator.
 310 class_op1_from
 311  :: forall root ty cl ex ast hs ret.
 312  ( ty ~ Type_Root_of_Expr ex
 313  , root ~ Root_of_Expr ex
 314  , Eq_Type ty
 315  , Expr_from ast root
 316  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 317                    (Error_of_Expr ast root)
 318  , Root_of_Expr root ~ root
 319  , Constraint_Type cl ty
 320  ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit)
 321  -> Proxy cl -> ast
 322  -> Expr_From ast ex hs ret
 323 class_op1_from op cl ast_x ex _ast ctx k =
 324         expr_from (Proxy::Proxy root) ast_x ctx $
 325          \ty_x (Forall_Repr_with_Context x) ->
 326         check_constraint_type ex cl ast_x ty_x $ \Dict ->
 327         k ty_x $ Forall_Repr_with_Context (op . x)
 328
 329 -- | Parse a binary class operator.
 330 class_op2_from
 331  :: forall root ty cl ex ast hs ret.
 332  ( ty ~ Type_Root_of_Expr ex
 333  , root ~ Root_of_Expr ex
 334  , Eq_Type ty
 335  , Expr_from ast root
 336  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 337                    (Error_of_Expr ast root)
 338  , Root_of_Expr root ~ root
 339  , Constraint_Type cl ty
 340  ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
 341  -> Proxy cl -> ast -> ast
 342  -> Expr_From ast ex hs ret
 343 class_op2_from op cl ast_x ast_y ex ast ctx k =
 344         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 345         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
 346         check_constraint_type ex cl ast_x ty_x $ \Dict ->
 347         check_constraint_type ex cl ast_y ty_y $ \Dict ->
 348         check_eq_type ex ast ty_x ty_y $ \Refl ->
 349         k ty_x $ Forall_Repr_with_Context $
 350          \c -> x c `op` y c
 351
 352 -- | Parse a unary operator.
 353 op1_from
 354  :: forall root ty lit ex ast hs ret.
 355  ( ty ~ Type_Root_of_Expr ex
 356  , root ~ Root_of_Expr ex
 357  , Eq_Type ty
 358  , Expr_from ast root
 359  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 360                    (Error_of_Expr ast root)
 361  , Root_of_Expr root ~ root
 362  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 363  -> ty lit -> ast
 364  -> Expr_From ast ex hs ret
 365 op1_from op ty_lit ast_x ex ast ctx k =
 366         expr_from (Proxy::Proxy root) ast_x ctx $
 367          \ty_x (Forall_Repr_with_Context x) ->
 368         check_eq_type ex ast ty_lit ty_x $ \Refl ->
 369                 k ty_x $ Forall_Repr_with_Context (op . x)
 370
 371 -- | Parse a binary operator.
 372 op2_from
 373  :: forall root ty lit ex ast hs ret.
 374  ( ty ~ Type_Root_of_Expr ex
 375  , root ~ Root_of_Expr ex
 376  , Eq_Type ty
 377  , Expr_from ast root
 378  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 379                    (Error_of_Expr ast root)
 380  , Root_of_Expr root ~ root
 381  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 382  -> ty lit -> ast -> ast
 383  -> Expr_From ast ex hs ret
 384 op2_from op ty_lit ast_x ast_y ex ast ctx k =
 385         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 386         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
 387         check_eq_type ex ast ty_lit ty_x $ \Refl ->
 388         check_eq_type ex ast ty_lit ty_y $ \Refl ->
 389                 k ty_x $ Forall_Repr_with_Context $
 390                  \c -> x c `op` y c