Language/LOL/Symantic/Expr/Eq.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE ScopedTypeVariables #-}
   4 {-# LANGUAGE TypeFamilies #-}
   5 -- | Expression for 'Eq'.
   6 module Language.LOL.Symantic.Expr.Eq where
   7
   8 import Data.Proxy (Proxy(..))
   9 import Data.Type.Equality ((:~:)(Refl))
  10
  11 import Language.LOL.Symantic.Repr.Dup
  12 import Language.LOL.Symantic.Trans.Common
  13 import Language.LOL.Symantic.Type
  14 import Language.LOL.Symantic.Expr.Common
  15 import Language.LOL.Symantic.Expr.Lambda
  16 import Language.LOL.Symantic.Expr.Bool
  17
  18 -- * Class 'Sym_Eq'
  19
  20 class Sym_Eq repr where
  21         eq :: Eq a => repr a -> repr a -> repr Bool
  22         default eq :: (Trans t repr, Eq a)
  23                    => t repr a -> t repr a -> t repr Bool
  24         eq = trans_map2 eq
  25
  26 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where
  27         eq (x1 `Dup` x2) (y1 `Dup` y2) = eq x1 y1 `Dup` eq x2 y2
  28
  29 -- * Type 'Expr_Eq'
  30 -- | Expression.
  31 data Expr_Eq (root:: *)
  32 type instance Root_of_Expr      (Expr_Eq root)      = root
  33 type instance Type_of_Expr      (Expr_Eq root)      = No_Type
  34 type instance Sym_of_Expr       (Expr_Eq root) repr = (Sym_Eq repr)
  35 type instance Error_of_Expr ast (Expr_Eq root)      = No_Error_Expr
  36
  37 eq_from
  38  :: forall root ty ast hs ret.
  39  ( ty ~ Type_Root_of_Expr (Expr_Eq root)
  40  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  41  , Type_Eq (Type_Root_of_Expr root)
  42  , Expr_from ast root
  43  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  44                    (Error_of_Expr ast root)
  45  , Root_of_Expr root ~ root
  46  , Type_Constraint Eq ty
  47  ) => ast -> ast
  48  -> Expr_From ast (Expr_Eq root) hs ret
  49 eq_from ast_x ast_y ex ast ctx k =
  50         expr_from (Proxy::Proxy root) ast_x ctx $
  51          \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
  52         expr_from (Proxy::Proxy root) ast_y ctx $
  53          \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
  54         when_type_eq ex ast ty_x ty_y $ \Refl ->
  55         when_type_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
  56                 k type_bool $ Forall_Repr_with_Context $
  57                  \c -> x c `eq` y c
  58
  59 -- ** Type 'Expr_Lambda_Bool_Eq'
  60 -- | Convenient alias.
  61 type Expr_Lambda_Bool_Eq lam
  62  = Expr_Root (Expr_Alt (Expr_Lambda lam)
  63              (Expr_Alt Expr_Bool
  64                        Expr_Eq))
  65
  66 -- | Convenient alias around 'expr_from'.
  67 expr_lambda_bool_eq_from
  68  :: forall lam ast.
  69  Expr_from ast (Expr_Lambda_Bool_Eq lam)
  70  => Proxy lam
  71  -> ast
  72  -> Either (Error_of_Expr ast (Expr_Lambda_Bool_Eq lam))
  73            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool_Eq lam))
  74                                  (Forall_Repr (Expr_Lambda_Bool_Eq lam)))
  75 expr_lambda_bool_eq_from _lam ast =
  76         expr_from (Proxy::Proxy (Expr_Lambda_Bool_Eq lam)) ast
  77          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
  78                 Right $ Exists_Type_and_Repr ty $
  79                         Forall_Repr $ repr Context_Empty