{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DefaultSignatures #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-module Language.Symantic.Compiling.Term where
+module Language.Symantic.Compiling.Term
+ ( module Language.Symantic.Compiling.Term
+ , module Language.Symantic.Compiling.Term.Grammar
+ ) where
-import qualified Data.Function as Fun
import qualified Data.Kind as Kind
-import Data.Kind hiding (Type)
-import Data.Monoid ((<>))
import Data.Proxy (Proxy(..))
-import Data.String (IsString)
-import Data.Text (Text)
import qualified Data.Text as Text
-import Data.Type.Equality
+import Data.Type.Equality ((:~:)(..))
import GHC.Exts (Constraint)
-import Prelude hiding (not)
-import Language.Symantic.Lib.Data.Type.List
+import Language.Symantic.Helper.Data.Type.List
+import Language.Symantic.Parsing
import Language.Symantic.Typing
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming.Trans
+
+import Language.Symantic.Compiling.Term.Grammar
-- * Type 'Term'
--- | 'TermLC' applied on a 'LamCtx_Type'.
+-- | Closed 'TermO'.
data Term is h
= Term
(forall term. ( Sym_of_Ifaces is term
- , Sym_Lambda term
+ , Sym_of_Iface (Proxy (->)) term
) => term h)
--- ** Type 'TermLC'
--- | A data type embedding a universal quantification
+-- ** Type 'TermO'
+-- | An open term (i.e. with a /lambda context/).
+-- The data type wraps a universal quantification
-- over an interpreter @term@
--- and qualified by the symantics of a term.
+-- qualified by the symantics of a term.
--
-- Moreover the term is abstracted by a 'LamCtx_Term'
--- built top-down at parsing time
--- to build a /Higher-Order Abstract Syntax/ (HOAS)
+-- built top-down by 'compileO',
+-- to enable a /Higher-Order Abstract Syntax/ (HOAS)
-- for /lambda abstractions/ ('lam').
--
-- This data type is used to keep a parsed term polymorphic enough
--
-- * @(@'Sym_of_Ifaces'@ is term)@
-- is needed when a symantic method includes a polymorphic type
--- and thus calls: 'term_from'.
+-- and thus calls: 'compileO'.
--
-- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
--- are needed to be able to write the instance:
--- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
+-- make a zipper needed to be able to write the recursing 'CompileR' instance.
--
--- * @(@'Sym_Lambda'@ term)@
--- is needed to be able to parse partially applied functions
--- (when their type is knowable).
-data TermLC ctx h is ls rs
- = TermLC
+-- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
+-- is needed to handle partially applied functions.
+data TermO ctx h is ls rs
+ = TermO
(forall term. ( Sym_of_Ifaces is term
, Sym_of_Ifaces ls term
, Sym_of_Ifaces rs term
- , Sym_Lambda term
+ , Sym_of_Iface (Proxy (->)) term
) => LamCtx_Term term ctx -> term h)
-- * Type 'ETerm'
(Type (Consts_of_Ifaces is) h)
(Term is h)
--- | Like 'term_from' but for a term with an empty /lambda context/.
-root_term_from
- :: Term_from is ast
- => ast -> Either (Error_Term is ast) (ETerm is)
-root_term_from ast =
- term_from ast LamCtx_TypeZ $ \ty (TermLC te) ->
- Right $ ETerm ty $ Term $ te LamCtx_TermZ
-
--- * Type 'Term_from'
--- | Convenient type synonym wrapping 'Term_fromR'
--- to initiate its recursion.
-class Term_from is ast where
- term_from :: Term_fromT ast ctx ret is '[] is
-instance
- ( AST ast
- , Eq (Lexem ast)
- , Term_fromR is '[] is ast
- ) => Term_from is ast where
- term_from ast ctx k =
- case replace_var (ast_lexem ast) ctx k of
- Left Error_Term_unsupported -> term_fromR ast ctx k
- x -> x
- where
- replace_var :: forall lc ret.
- Lexem ast
- -> LamCtx_Type is (Lexem ast) lc
- -> ( forall h.
- Type (Consts_of_Ifaces is) (h::Kind.Type)
- -> TermLC lc h is '[] is
- -> Either (Error_Term is ast) ret )
- -> Either (Error_Term is ast) ret
- replace_var name lc k' =
- case lc of
- LamCtx_TypeZ -> Left $ Error_Term_unsupported
- LamCtx_TypeS n ty _ | n == name ->
- k' ty $ TermLC $ \(te `LamCtx_TermS` _) -> te
- LamCtx_TypeS _n _ty lc' ->
- replace_var name lc' $ \ty (TermLC te::TermLC lc' h is '[] is) ->
- k' ty $ TermLC $ \(_ `LamCtx_TermS` c) -> te c
-
--- ** Type 'Term_fromT'
+-- * Type 'Compile'
+-- | Convenient type synonym wrapping 'CompileR' to initiate its recursion.
+class Compile is where
+ compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
+instance CompileR is '[] is => Compile is where
+ compileO (EToken tok) = compileR tok
+
+-- | Like 'compileO' minus for a term with an empty /lambda context/.
+compile
+ :: Compile is
+ => EToken meta is
+ -> Either (Error_Term meta is) (ETerm is)
+compile tok =
+ compileO tok LamCtx_TypeZ $ \typ (TermO te) ->
+ Right $ ETerm typ $ Term $ te LamCtx_TermZ
+
+-- ** Type 'CompileT'
-- | Convenient type synonym defining a term parser.
-type Term_fromT ast ctx ret is ls rs
- = ast
- -> LamCtx_Type is (Lexem ast) ctx
+type CompileT meta ctx ret is ls rs
+ = LamCtx_Type is Term_Name ctx
-- ^ The bound variables in scope and their types:
-- built top-down in the heterogeneous list @ctx@,
-- from the closest including /lambda abstraction/ to the farest.
-> ( forall h.
Type (Consts_of_Ifaces is) (h::Kind.Type)
- -> TermLC ctx h is ls rs
- -> Either (Error_Term is ast) ret )
+ -> TermO ctx h is ls rs
+ -> Either (Error_Term meta is) ret )
-- ^ The accumulating continuation called bottom-up.
- -> Either (Error_Term is ast) ret
+ -> Either (Error_Term meta is) ret
--- ** Class 'Term_fromR'
--- | Intermediate type class to construct an instance of 'Term_from'
--- from many instances of 'Term_fromI', one for each item of @is@.
+-- ** Class 'CompileR'
+-- | Intermediate type class to construct an instance of 'Compile'
+-- from many instances of 'CompileI', one for each item of @is@.
--
-- * @is@: starting list of /term constants/.
-- * @ls@: done list of /term constants/.
-- * @rs@: remaining list of /term constants/.
-class Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
- term_fromR :: Term_fromT ast ctx ret is ls rs
- default term_fromR :: AST ast => Term_fromT ast ctx ret is ls rs
- term_fromR ast _ctx _k =
- Left $ Error_Term_unknown $
- At (Just ast) $ ast_lexem ast
+class CompileR (is::[*]) (ls::[*]) (rs::[*]) where
+ compileR :: TokenR meta is rs i -> CompileT meta ctx ret is ls rs
--- | Test whether @i@ handles the work of 'Term_from' or not,
--- or recurse on @rs@, preserving the starting list of /term constants/,
--- and keeping a list of those done to construct 'TermLC'.
+-- | Recurse into into the given 'TokenR'
+-- to call the 'compileI' instance associated
+-- to the 'TokenT' it contains.
instance
- ( Term_fromI is i ast
- , Term_fromR is (i ': ls) rs ast
- ) => Term_fromR is ls (i ': rs) ast where
- term_fromR ast ctx k =
- case term_fromI ast ctx $ \ty (TermLC te
- ::TermLC ctx h is ls (i ': rs)) ->
- k ty (TermLC te) of
- Left Error_Term_unsupported ->
- term_fromR ast ctx $ \ty (TermLC te
- ::TermLC ctx h is (i ': ls) rs) ->
- k ty (TermLC te
- ::TermLC ctx h is ls (i ': rs))
- x -> x
+ ( CompileI is i
+ , CompileR is (i ': ls) (r ': rs)
+ ) => CompileR is ls (i ': r ': rs) where
+ compileR tok ctx k =
+ case tok of
+ TokenZ _m t -> compileI t ctx k
+ TokenS t ->
+ compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
+ k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
-- | End the recursion.
-instance AST ast => Term_fromR is ls '[] ast
+instance
+ CompileI is i =>
+ CompileR is ls (i ': '[]) where
+ compileR (TokenZ _m t) ctx k = compileI t ctx k
+ compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."
--- ** Class 'Term_fromI'
--- | Handle the work of 'Term_from' for a given /interface/ @i@,
--- that is: maybe it handles the given /interface/,
--- and if so, maybe the term can be parsed.
-class Term_fromI (is::[*]) (i:: *) ast where
- term_fromI :: Term_fromT ast ctx ret is ls (i ': rs)
- term_fromI _ast _ctx _k = Left $ Error_Term_unsupported
+-- ** Class 'CompileI'
+-- | Handle the work of 'Compile' for a given /interface/ @i@.
+class CompileI (is::[*]) (i:: *) where
+ compileI :: TokenT meta is i -> CompileT meta ctx ret is ls (i ': rs)
-- * Type family 'Sym_of_Ifaces'
type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
-- ** Type family 'Consts_of_Iface'
-type family Consts_of_Iface (i::k) :: [*]
+type family Consts_of_Iface (i:: *) :: [*]
type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
-- * Type 'LamCtx_Type'
-> LamCtx_Type is name (h ': hs)
infixr 5 `LamCtx_TypeS`
--- ** Type 'LamVarName'
-type LamVarName = Text
-
-- * Type 'LamCtx_Term'
data LamCtx_Term (term:: * -> *) (ctx::[*]) where
LamCtx_TermZ :: LamCtx_Term term '[]
infixr 5 `LamCtx_TermS`
-- * Type 'Error_Term'
-data Error_Term (is::[*]) ast
- = Error_Term_unknown (At ast (Lexem ast))
- | Error_Term_unsupported
- | Error_Term_Syntax (Error_Syntax ast)
- | Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) Constraint))
- | Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
- | Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
- (At ast (EType (Consts_of_Ifaces is)))
- | Error_Term_Type_is_not_an_application (At ast (EType (Consts_of_Ifaces is)))
-deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
-deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)
-
-instance Lift_Error_Syntax (Error_Term is) where
- lift_error_syntax = Error_Term_Syntax
+data Error_Term meta (is::[*])
+ = Error_Term_unbound Term_Name
+ | Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
+ | Error_Term_Constraint_Type
+ (Either
+ (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
+ (Constraint_Type meta is (Consts_of_Ifaces is)))
+ | Error_Term_Constraint_Kind (Constraint_Kind meta is)
+deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
+deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)
+
+-- * Type 'Constraint_Type'
+data Constraint_Type meta ts cs
+ = Constraint_Type_Eq (Either (At meta '[Proxy Token_Type] (EType cs))
+ (At meta ts (EType cs)))
+ (At meta ts (EType cs))
+ | Constraint_Type_App (At meta ts (EType cs))
+ | Constraint_Type_Con (At meta ts (KType cs Constraint))
+ | Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
+deriving instance
+ ( Eq meta
+ , Eq_Token meta ts
+ ) => Eq (Constraint_Type meta ts cs)
+deriving instance
+ ( Show meta
+ , Show_Token meta ts
+ , Show_Const cs
+ ) => Show (Constraint_Type meta ts cs)
+
+instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
+ olift = Error_Term_Typing . olift
+instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
+ olift = Prelude.id
+instance
+ cs ~ Consts_of_Ifaces is =>
+ MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
+ olift = Error_Term_Constraint_Type . Right
+instance
+ cs ~ Consts_of_Ifaces is =>
+ MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
+ olift = Error_Term_Constraint_Type . Left
+instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
+ olift = Error_Term_Typing . Error_Type_Constraint_Kind
+instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
+ olift = Error_Term_Constraint_Kind
-- ** Checks
-
--- | Check that the 'kind_of' a given 'Type's equals a given kind,
--- or fail with 'Error_Type_Kind_mismatch'.
-check_kind
- :: ast -> SKind k
- -> At ast (Type (Consts_of_Ifaces is) (t::kt))
- -> ((k :~: kt) -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_kind ast ki (At at_ty ty) k =
- let ki_ty = kind_of ty in
- case eq_skind ki ki_ty of
- Just Refl -> k Refl
- Nothing -> Left $ Error_Term_Typing $
- At (Just ast) $
- Error_Type_Kind_mismatch
- (At Nothing $ EKind SKiType)
- (At at_ty $ EKind ki_ty)
-
--- | Check that a given 'Type' is a /type application/,
--- or fail with 'Error_Term_Type_is_not_an_application'.
-check_app
- :: ast -> Type (Consts_of_Ifaces is) (fx::kfx)
- -> (forall kx f x. (fx :~: f x)
- -> Type (Consts_of_Ifaces is) (f::kx -> kfx)
- -> Type (Consts_of_Ifaces is) (x::kx)
- -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_app ast ty_fx k =
- case ty_fx of
- ty_f :$ ty_x -> k Refl ty_f ty_x
- _ -> Left $ Error_Term_Type_is_not_an_application $
- At (Just ast) $ EType ty_fx
-
--- | Check that two given 'Type's are equal,
--- or fail with 'Error_Term_Type_mismatch'.
check_type
- :: At ast (Type (Consts_of_Ifaces is) x)
- -> At ast (Type (Consts_of_Ifaces is) y)
- -> ((x :~: y) -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_type (At at_x x) (At at_y y) k =
- case eq_type x y of
+ :: MonoLift (Constraint_Type meta ts cs) err
+ => At meta ts (Type cs x)
+ -> At meta ts (Type cs y)
+ -> ((x :~: y) -> Either err ret) -> Either err ret
+check_type x y k =
+ case unAt x `eq_type` unAt y of
+ Just Refl -> k Refl
+ Nothing -> Left $ olift $
+ Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)
+
+check_type_is
+ :: MonoLift (Constraint_Type meta ts cs) err
+ => At meta '[Proxy Token_Type] (Type cs x)
+ -> At meta ts (Type cs y)
+ -> ((x :~: y) -> Either err ret) -> Either err ret
+check_type_is x y k =
+ case unAt x `eq_type` unAt y of
Just Refl -> k Refl
- Nothing -> Left $ Error_Term_Type_mismatch
- (At at_x $ EType x)
- (At at_y $ EType y)
+ Nothing -> Left $ olift $
+ Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)
+
+check_type_app
+ :: MonoLift (Constraint_Type meta ts cs) err
+ => At meta ts (Type cs (fa::kfa))
+ -> (forall ka f a. (fa :~: f a)
+ -> Type cs (f::ka -> kfa)
+ -> Type cs (a::ka)
+ -> Either err ret)
+ -> Either err ret
+check_type_app typ k =
+ case unAt typ of
+ a :$ b -> k Refl a b
+ _ -> Left $ olift $
+ Constraint_Type_App (EType <$> typ)
--- | Convenient wrapper to check for a 'Type' of kind: @* -> *@.
check_type1
- :: Type (Consts_of_Ifaces is) ty
- -> ast
- -> Type (Consts_of_Ifaces is) (fx:: *)
- -> (forall x. (fx :~: ty x)
- -> Type (Consts_of_Ifaces is) (x:: *)
- -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_type1 ty ast_ta ty_ta k =
- check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
- check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
- check_type (At Nothing ty) (At (Just ast_ta) ty_ta_t) $ \Refl ->
- k Refl ty_ta_a
+ :: ( MonoLift (Constraint_Type meta ts cs) err
+ , MonoLift (Constraint_Kind meta ts) err )
+ => Type cs (f:: * -> *)
+ -> At meta ts (Type cs fa)
+ -> (forall a. (fa :~: f a)
+ -> Type cs a
+ -> Either err ret)
+ -> Either err ret
+check_type1 typ ty_fa k =
+ check_type_app ty_fa $ \Refl ty_f ty_a ->
+ check_kind
+ (At Nothing $ SKiType `SKiArrow` SKiType)
+ (kind_of ty_f <$ ty_fa) $ \Refl ->
+ check_type
+ (At Nothing typ)
+ (ty_f <$ ty_fa) $ \Refl ->
+ k Refl ty_a
--- | Convenient wrapper to check for a 'Type' of kind: @* -> * -> *@.
check_type2
- :: Type (Consts_of_Ifaces is) (ty:: * -> * -> *)
- -> ast -> Type (Consts_of_Ifaces is) a2b
- -> (forall a b. (a2b :~: (ty a b))
- -> Type (Consts_of_Ifaces is) a
- -> Type (Consts_of_Ifaces is) b
- -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_type2 ty ast ty_a2b k =
- check_app ast ty_a2b $ \Refl ty_a2b_a2 ty_a2b_b ->
- check_app ast ty_a2b_a2 $ \Refl ty_a2b_ty ty_a2b_a ->
- check_kind ast (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) (At (Just ast) ty_a2b_ty) $ \Refl ->
- check_type (At Nothing ty) (At (Just ast) ty_a2b_ty) $ \Refl ->
- k Refl ty_a2b_a ty_a2b_b
-
--- | Check that a given 'Constraint' holds,
--- or fail with 'Error_Term_Constraint_not_deductible'.
-check_constraint
- :: Proj_Con (Consts_of_Ifaces is)
- => At ast (Type (Consts_of_Ifaces is) (q::Constraint))
- -> (Con q -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_constraint (At at_q q) k =
- case proj_con q of
+ :: ( MonoLift (Constraint_Type meta ts cs) err
+ , MonoLift (Constraint_Kind meta ts) err )
+ => Type cs (f:: * -> * -> *)
+ -> At meta ts (Type cs fab)
+ -> (forall a b. (fab :~: f a b)
+ -> Type cs a
+ -> Type cs b
+ -> Either err ret)
+ -> Either err ret
+check_type2 typ ty_fab k =
+ check_type_app ty_fab $ \Refl ty_fa ty_b ->
+ check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f ty_a ->
+ check_kind
+ (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
+ (kind_of ty_f <$ ty_fab) $ \Refl ->
+ check_type
+ (At Nothing typ)
+ (ty_f <$ ty_fab) $ \Refl ->
+ k Refl ty_a ty_b
+
+check_con
+ :: ( Proj_Con cs
+ , MonoLift (Constraint_Type meta ts cs) err )
+ => At meta ts (Type cs (q::Constraint))
+ -> (Con q -> Either err ret)
+ -> Either err ret
+check_con typ k =
+ case proj_con $ unAt typ of
Just Con -> k Con
- Nothing -> Left $ Error_Term_Constraint_not_deductible $
- At at_q $ KType q
-
--- | Convenient wrapper to check for a 'Constraint'
--- over a 'Type' of kind: @* -> *@.
-check_constraint1
- :: Proj_Con (Consts_of_Ifaces is)
- => Type (Consts_of_Ifaces is) con
- -> ast -> Type (Consts_of_Ifaces is) (fx:: *)
- -> (forall f x. (fx :~: f x)
+ Nothing -> Left $ olift $
+ Constraint_Type_Con (KType <$> typ)
+
+check_con1
+ :: ( Proj_Con cs
+ , MonoLift (Constraint_Type meta ts cs) err
+ , MonoLift (Constraint_Kind meta ts) err )
+ => Type cs con
+ -> At meta ts (Type cs (fa:: *))
+ -> (forall f a. (fa :~: f a)
-> Con (con f)
- -> Type (Consts_of_Ifaces is) (f:: * -> *)
- -> Type (Consts_of_Ifaces is) (x:: *)
- -> Either (Error_Term is ast) ret)
- -> Either (Error_Term is ast) ret
-check_constraint1 con ast_ta ty_ta k =
- check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
- check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
- check_constraint (At (Just ast_ta) (con :$ ty_ta_t)) $ \Con ->
- k Refl Con ty_ta_t ty_ta_a
-
--- * Class 'Sym_Lambda'
-class Sym_Lambda term where
- -- | /Lambda abstraction/.
- lam :: (term arg -> term res) -> term ((->) arg res)
- default lam :: Trans t term
- => (t term arg -> t term res)
- -> t term ((->) arg res)
- lam f = trans_lift $ lam $ trans_apply . f . trans_lift
-
- -- | /Lambda application/.
- (.$) :: term ((->) arg res) -> term arg -> term res
- default (.$) :: Trans t term
- => t term ((->) arg res) -> t term arg -> t term res
- (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
-
- -- | Convenient 'lam' and '.$' wrapper.
- let_ :: term var -> (term var -> term res) -> term res
- let_ x y = lam y .$ x
-
- id :: term a -> term a
- id a = lam Fun.id .$ a
-
- const :: term a -> term b -> term a
- const a b = lam (lam . Fun.const) .$ a .$ b
-
- -- | /Lambda composition/.
- (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
- (#) f g = lam $ \a -> f .$ (g .$ a)
-
- flip :: term (a -> b -> c) -> term (b -> a -> c)
- flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
-
-infixl 0 .$
-infixr 9 #
-
-type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
-type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
-type instance Consts_imported_by (->) =
- [ Proxy Applicative
- , Proxy Functor
- , Proxy Monad
- , Proxy Monoid
- ]
-
-instance Sym_Lambda HostI where
- lam f = HostI (unHostI . f . HostI)
- (.$) = (<*>)
-instance Sym_Lambda TextI where
- lam f = TextI $ \p v ->
- let p' = Precedence 1 in
- let x = "x" <> Text.pack (show v) in
- paren p p' $ "\\" <> x <> " -> "
- <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
- -- (.$) = textI_infix "$" (Precedence 0)
- (.$) (TextI a1) (TextI a2) =
- TextI $ \p v ->
- let p' = precedence_App in
- paren p p' $ a1 p' v <> " " <> a2 p' v
- let_ e in_ =
- TextI $ \p v ->
- let p' = Precedence 2 in
- let x = "x" <> Text.pack (show v) in
- paren p p' $ "let" <> " " <> x <> " = "
- <> unTextI e (Precedence 0) (succ v) <> " in "
- <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
- (#) = textI_infix "." (Precedence 9)
- id = textI_app1 "id"
- const = textI_app2 "const"
- flip = textI_app1 "flip"
-instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
- lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
- where lam_f = lam f
- (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
-
-instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
- const_from "(->)" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
- show_const ConstZ{} = "(->)"
- show_const (ConstS c) = show_const c
-
-instance -- Proj_ConC (->)
- ( Proj_Const cs (->)
- , Proj_Consts cs (Consts_imported_by (->))
- , Proj_Con cs
- ) => Proj_ConC cs (Proxy (->)) where
- proj_conC _ (TyConst q :$ (TyConst c :$ _r))
- | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_const c (Proxy::Proxy (->))
- = Just $ case () of
- _ | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
- | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
- | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con
- _ -> Nothing
- proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
- | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_const c (Proxy::Proxy (->))
- = Just $ case () of
- _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
- , Just Con <- proj_con (t :$ b) -> Just Con
- _ -> Nothing
- proj_conC _c _q = Nothing
-instance -- Term_fromI (->)
- ( AST ast
- , Lexem ast ~ LamVarName
- , Inj_Const (Consts_of_Ifaces is) (->)
- , Const_from (Lexem ast) (Consts_of_Ifaces is)
- , Term_from is ast
- ) => Term_fromI is (Proxy (->)) ast where
- term_fromI ast ctx k =
- case ast_lexem ast of
- "\\" ->
- from_ast3 ast $ \ast_name ast_ty_arg ast_body ->
- either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
- type_from ast_ty_arg $ \ty_arg -> Right $
- check_kind ast SKiType (At (Just ast) ty_arg) $ \Refl ->
- term_from ast_body
- (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
- \ty_res (TermLC res) ->
- k (ty_arg ~> ty_res) $ TermLC $
- \c -> lam $ \arg ->
- res (arg `LamCtx_TermS` c)
- " " ->
- from_ast2 ast $ \ast_lam ast_arg_actual ->
- term_from ast_lam ctx $ \ty_lam (TermLC lam_) ->
- term_from ast_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
- check_type2 tyFun ast_lam ty_lam $ \Refl ty_arg ty_res ->
- check_type
- (At (Just ast_lam) ty_arg)
- (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
- k ty_res $ TermLC $
- \c -> lam_ c .$ arg_actual c
- "let" ->
- from_ast3 ast $ \ast_name ast_bound ast_body ->
- term_from ast_bound ctx $ \ty_bound (TermLC bound) ->
- term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_bound ctx) $
- \ty_res (TermLC res) ->
- k ty_res $ TermLC $
- \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
- _ -> Left $ Error_Term_unsupported
-
--- | The '(->)' 'Type'
-tyFun :: Inj_Const cs (->) => Type cs (->)
-tyFun = TyConst inj_const
-
--- | The function 'Type' @(->)@,
--- with an infix notation more readable.
-(~>) :: forall cs a b. Inj_Const cs (->)
- => Type cs a -> Type cs b -> Type cs (a -> b)
-(~>) a b = tyFun :$ a :$ b
-infixr 5 ~>
-
-syFun :: IsString a => [Syntax a] -> Syntax a
-syFun = Syntax "(->)"
-
-(.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
-a .> b = syFun [a, b]
-infixr 3 .>
-
-syLam :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
-syLam arg ty body = Syntax "\\" [arg, ty, body]
-
-syApp :: IsString a => Syntax a -> Syntax a -> Syntax a
-syApp lam_ arg = Syntax " " [lam_, arg]
-infixl 0 `syApp`
-
-syLet :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
-syLet name bound body = Syntax "let" [name, bound, body]
-
-{-
--- * Checks
-
--- | Parsing utility to check that the type resulting
--- from the application of a given type family to a given type
--- is within the type stack,
--- or raise 'Error_Term_Type_mismatch'.
-check_type0_family
- :: forall ast is tf root ty h ret.
- ( root ~ Root_of_Expr is
- , ty ~ Type_Root_of_Expr is
- , Type0_Family tf ty
- , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
- (Error_of_Expr ast root)
- ) => Proxy tf -> Proxy is -> ast -> ty h
- -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
- -> Either (Error_of_Expr ast root) ret
-check_type0_family tf is ast ty k =
- case type0_family tf ty of
+ -> Type cs (f:: * -> *)
+ -> Type cs (a:: *)
+ -> Either err ret)
+ -> Either err ret
+check_con1 con ty_fa k =
+ check_type_app ty_fa $ \Refl ty_f ty_a ->
+ check_kind
+ (At Nothing (SKiType `SKiArrow` SKiType))
+ (kind_of ty_f <$ ty_fa) $ \Refl ->
+ check_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
+ k Refl Con ty_f ty_a
+
+check_fam
+ :: ( MonoLift (Constraint_Type meta ts cs) err
+ , Proj_Fam cs fam
+ , Show fam )
+ => At meta ts fam
+ -> Types cs hs
+ -> (Type cs (Fam fam hs) -> Either err ret)
+ -> Either err ret
+check_fam fam tys k =
+ case proj_fam (unAt fam) tys of
Just t -> k t
- Nothing -> Left $ error_expr is $
- Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
-
--}
+ Nothing -> Left $ olift $
+ Constraint_Type_Fam
+ (Text.pack . show <$> fam)
+ (etypes tys)