data AST
= AST Text [AST]
deriving (Eq)
+-- | Custom 'Show' instance a little bit more readable
+-- than the automatically derived one.
instance Show AST where
showsPrec p ast@(AST f args) =
let n = Text.unpack f in
case ast of
AST _ [] -> showString n
- AST "->" _ ->
- case args of
- [a] ->
+ AST "->" [a] ->
showParen (p >= 1) $
showString ("("++n++") ") .
showsPrec 1 a
- [a, b] ->
+ AST "->" [a, b] ->
showParen (p >= 1) $
showsPrec 1 a .
showString (" "++n++" ") .
-- * Class 'Sym_Bool'
--- | Symantic for 'Bool's.
+-- | Symantic.
class Sym_Bool repr where
bool :: Bool -> repr Bool
not :: repr Bool -> repr Bool
xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
-- * Type 'Expr_Bool'
--- | Expression's extension.
+-- | Expression.
data Expr_Bool (root:: *)
type instance Root_of_Expr (Expr_Bool root) = root
type instance Type_of_Expr (Expr_Bool root) = Type_Bool
( Type_Root_of_Expr root)
AST)
(Error_of_Expr AST root)
- , Error_Expr_Lift (Error_Expr_Read AST)
- (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr AST) (Error_of_Expr AST root)
, Type_Unlift Type_Bool (Type_of_Expr root)
case asts of
[AST ast_bool []] ->
case read_safe ast_bool of
- Left err -> Left $ Just $ error_expr_lift
- (Error_Expr_Read err ast :: Error_Expr_Read AST)
+ Left err -> Left $ error_expr_lift $ Error_Expr_Read err ast
Right (i::Bool) ->
k type_bool $ Forall_Repr_with_Context $
const $ bool i
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
AST "not" asts -> unary_from asts not
AST "and" asts -> binary_from asts and
AST "or" asts -> binary_from asts or
AST "xor" asts -> binary_from asts xor
- _ -> Left Nothing
+ _ -> Left $ error_expr_lift $ Error_Expr_Unsupported ast
where
unary_from asts
(op::forall repr. Sym_Bool repr
case type_unlift $ unType_Root ty_x of
Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
k ty_x $ Forall_Repr_with_Context (op . x)
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_bool)
(Exists_Type ty_x) ast
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 1 ast
binary_from asts
(op::forall repr. Sym_Bool repr
Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_y) ->
k ty_x $ Forall_Repr_with_Context $
\c -> x c `op` y c
- Nothing -> Left $ Just $ error_lambda_lift $
+ Nothing -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_bool)
(Exists_Type ty_y) ast
- Nothing -> Left $ Just $ error_lambda_lift $
+ Nothing -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_bool)
(Exists_Type ty_x) ast
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 2 ast
error_lambda_lift
:: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
Expr_from ast (Expr_Lambda_Bool lam)
=> Proxy lam
-> ast
- -> Either (Maybe (Error_of_Expr ast (Expr_Lambda_Bool lam)))
+ -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
(Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
(Forall_Repr (Expr_Lambda_Bool lam)))
expr_lambda_bool_from _px_lam ast =
e8 = x `xor` (y `xor` bool True)
-- * Tests
-(==>) :: forall h raw.
+(==>) :: forall h raw root.
( Eq h, Eq raw, Show h, Show raw
- , Expr_from raw (Expr_Lambda IO (Expr_Lambda_Bool IO))
- , Expr_from raw (Expr_Bool (Expr_Lambda_Bool IO)))
+ , root ~ Expr_Lambda_Bool IO
+ , Expr_from raw (Expr_Lambda IO root)
+ , Expr_from raw (Expr_Bool root)
+ -- , Error_Type_Lift (Error_Type raw) (Error_of_Type raw (Type_Root_of_Expr (Expr_Lambda_Bool IO))))
+ -- , Error_Type_Lift (Error_Type raw) err_ty0
+ )
=> raw -> (Type_Fun_Bool IO h, h, String) -> TestTree
(==>) raw expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
testCase (show raw) $
Left err -> return $ Left err
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case ty `type_eq` ty_expected of
- Nothing -> return $ Left $ Nothing -- Just $ "Type mismatch"
+ Nothing -> return $ Left $
+ error_lambda_lift $ Error_Expr_Type
+ (error_type_lift $ Error_Type_Unsupported raw) raw
Just Refl -> do
h <- host_from_expr r
return $
, string_from_expr r
-- , (string_from_expr :: Repr_String IO h -> String) r
)
+ where
+ error_lambda_lift
+ :: (root ~ Expr_Lambda_Bool IO)
+ => Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root))
+ (Type_Root_of_Expr root)
+ raw
+ -> Error_of_Expr raw root
+ error_lambda_lift = error_expr_lift
tests :: TestTree
tests = testGroup "Bool" $
:: forall hs ret
. Proxy ex
-- ^ Select the 'Expr_from' instance for the expression @ex@.
- -> Context (Var (Root_of_Expr ex)) hs
- -- ^ The bound variables and their types held in the heterogeneous list @hs@
- -- (types being constructed within: 'Type_Root_of_Expr' @ex@.
+ -> Context (Var (Type_Root_of_Expr ex)) hs
+ -- ^ The bound variables in scope and their types:
+ -- held in the heterogeneous list @hs@,
+ -- from the closest including lambda abstraction to the farest.
-> ast
-- ^ The input data to parse.
-> ( forall h
. Type_Root_of_Expr ex h
- -- The type of the parsed expression.
-> Forall_Repr_with_Context ex hs h
- -- The parsed expression
- -- (still abstracted by a 'Context' at this point).
- -> Either (Maybe (Error_of_Expr ast (Root_of_Expr ex))) ret
- )
+ -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
-- ^ The accumulating continuation.
- -> Either (Maybe (Error_of_Expr ast (Root_of_Expr ex))) ret
+ -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
-- ** Type 'Context'
infixr 5 `Context_Next`
-- ** Type 'Var'
--- | Join a name and a type;
--- used to handle lambda variables by name
+-- | Join a name and a type.
+--
+-- This data type is used to handle lambda variables by name
-- (instead of DeBruijn indices for instance).
-data Var ex h
- = Var Var_Name (Type_Root_of_Expr ex h)
+data Var ty h
+ = Var Var_Name (ty h)
type Var_Name = Text
-- ** Type 'Forall_Repr_with_Context'
--- | A data type embedding a universal quantification over @repr@
--- to construct an expression polymorphic enough to stay
--- interpretable by different interpreters;
--- moreover the expression is abstracted by a 'Context'
--- built at parsing time.
+-- | A data type embedding a universal quantification
+-- over an interpreter @repr@
+-- and qualified by the symantics of an expression.
+--
+-- Moreover the expression is abstracted by a 'Context'
+-- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
+-- for lambda abstractions.
+--
+-- This data type is used to keep a parsed expression polymorphic enough
+-- to stay interpretable by different interpreters.
+--
+-- NOTE: 'Sym_of_Expr'@ ex repr@
+-- is needed to be able to use symantic methods of the parsed expression
+-- into a 'Forall_Repr_with_Context' @ex@.
+--
+-- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
+-- is needed to be able to use an expression
+-- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
+-- into a 'Forall_Repr_with_Context'@ ex@,
+-- which happens when a symantic method includes a polymorphic type.
data Forall_Repr_with_Context ex hs h
= Forall_Repr_with_Context
( forall repr. ( Sym_of_Expr ex repr
, Sym_of_Expr (Root_of_Expr ex) repr
) => Context repr hs -> repr h )
--- *** Type 'Forall_Repr'
+-- ** Type 'Forall_Repr'
data Forall_Repr ex h
= Forall_Repr
{ unForall_Repr :: forall repr
. Sym_of_Expr ex repr
=> repr h }
--- ** Type 'Root_of_Expr'
+-- ** Type family 'Root_of_Expr'
-- | The root expression, closing an expression with itself.
type family Root_of_Expr (ex:: *) :: *
--- ** Type 'Sym_of_Expr'
+-- ** Type family 'Sym_of_Expr'
-- | The symantic of an expression.
type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
--- ** Type 'Error_of_Expr'
+-- ** Type family 'Error_of_Expr'
-- | The error(s) of an expression.
type family Error_of_Expr (ast:: *) (ex:: *) :: *
--- ** Type 'Type_of_Expr'
+-- ** Type family 'Type_of_Expr'
-- | The type of an expression, parameterized by a root type.
type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
-- ** Type 'Type_Root_of_Expr'
+-- | Convenient alias.
type Type_Root_of_Expr ex
= Type_Root (Type_of_Expr (Root_of_Expr ex))
= Type_of_Expr (ex (Expr_Root ex))
-- NOTE: require UndecidableInstances.
type instance Error_of_Expr ast (Expr_Root ex)
- = Error_Expr_Cons (Error_Expr_Read ast)
- (Error_of_Expr ast (ex (Expr_Root ex)))
+ = Error_Expr_Cons (Error_Expr ast)
+ (Error_of_Expr ast (ex (Expr_Root ex)))
-- NOTE: require UndecidableInstances.
type instance Sym_of_Expr (Expr_Root ex) repr
= Sym_of_Expr (ex (Expr_Root ex)) repr
k ty (Forall_Repr_with_Context repr)
-- ** Class 'Expr_Root_Lift'
--- | Lift a given type to a given root type.
+-- | Lift a given expression to a given root expression.
class Expr_Root_Lift ex root where
expr_root_lift :: ex root -> root
instance
-- * Type 'Expr_Cons'
--- | Combine two types into one.
+-- | Combine two expressions into one.
data Expr_Cons curr next (root:: *)
= Expr_Curr (curr root)
| Expr_Next (next root)
, Expr_from ast (next root)
, Root_of_Expr (curr root) ~ root
, Root_of_Expr (next root) ~ root
+ , Error_Expr_Unlift (Error_Expr ast) (Error_of_Expr ast root)
) => Expr_from ast (Expr_Cons curr next root) where
expr_from _px_ex ctx ast k =
case expr_from (Proxy::Proxy (curr root)) ctx ast $
\ty (Forall_Repr_with_Context repr) ->
Right $ k ty (Forall_Repr_with_Context repr) of
Right ret -> ret
- Left Nothing -> expr_from (Proxy::Proxy (next root)) ctx ast $
- \ty (Forall_Repr_with_Context repr) ->
- k ty (Forall_Repr_with_Context repr)
- Left err -> Left err
+ Left err ->
+ case error_expr_unlift err of
+ Just (Error_Expr_Unsupported (_::ast)) ->
+ expr_from (Proxy::Proxy (next root)) ctx ast $
+ \ty (Forall_Repr_with_Context repr) ->
+ k ty (Forall_Repr_with_Context repr)
+ _ -> Left err
--- ** Type 'Peano_of_Expr'
+-- ** Type 'Expr_Lift'
+-- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
+type Expr_Lift ex exs
+ = Expr_LiftN (Peano_of_Expr ex exs) ex exs
+
+-- | Convenient wrapper around 'expr_liftN',
+-- passing it the 'Peano' number from 'Peano_of_Expr',
+-- used to avoid @OverlappingInstances@.
+expr_lift
+ :: forall ex exs (root:: *).
+ Expr_Lift ex exs =>
+ ex root -> exs root
+expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
+
+-- *** Type family 'Peano_of_Expr'
-- | Return a 'Peano' number derived from the location
--- of a given extension within a given extension stack.
+-- of a given expression within a given expression stack.
type family Peano_of_Expr
(ex:: * -> *)
(exs:: * -> *) :: Peano where
Peano_of_Expr ex (Expr_Cons ex next) = 'Zero
Peano_of_Expr other (Expr_Cons curr next) = 'Succ (Peano_of_Expr other next)
--- ** Type 'Expr_Lift'
--- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
-type Expr_Lift ex exs
- = Expr_LiftN (Peano_of_Expr ex exs) ex exs
-
-- *** Class 'Expr_LiftN'
--- | Construct the sequence of 'Expr_Curr' and 'Expr_Next'
--- lifting a given extension to the top of a given extension stack.
+-- | Lift a given expression to the top of a given expression stack including it,
+-- by constructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
class Expr_LiftN (n::Peano) ex exs where
expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
instance Expr_LiftN 'Zero curr curr where
Expr_LiftN ('Succ n) other (Expr_Cons curr next) where
expr_liftN _ = Expr_Next . expr_liftN (Proxy::Proxy n)
--- | Convenient wrapper around 'expr_liftN',
--- passing it the 'Peano' number from 'Peano_of_Expr'.
-expr_lift
- :: forall ex exs (root:: *).
- Expr_Lift ex exs =>
- ex root -> exs root
-expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
-
+{- NOTE: unused code so far
-- ** Type 'Expr_Unlift'
-- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
type Expr_Unlift ex exs
= Expr_UnliftN (Peano_of_Expr ex exs) ex exs
+-- | Convenient wrapper around 'expr_unliftN',
+-- passing it the 'Peano' number from 'Peano_of_Expr',
+-- used to avoid @OverlappingInstances@.
+expr_unlift
+ :: forall ex exs (root:: *).
+ Expr_Unlift ex exs =>
+ exs root -> Maybe (ex root)
+expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
+
-- *** Class 'Expr_UnliftN'
-- | Try to unlift a given expression out of a given expression stack including it,
-- by deconstructing the appropriate sequence of 'Expr_Curr' and 'Expr_Next'.
Expr_UnliftN ('Succ n) other (Expr_Cons curr next) where
expr_unliftN _ (Expr_Next x) = expr_unliftN (Proxy::Proxy n) x
expr_unliftN _ (Expr_Curr _) = Nothing
-
--- | Convenient wrapper around 'expr_unliftN',
--- passing it the 'Peano' number from 'Peano_of_Expr'.
-expr_unlift
- :: forall ex exs (root:: *).
- Expr_Unlift ex exs =>
- exs root -> Maybe (ex root)
-expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
+-}
-- * Type 'Error_Expr_Cons'
--- | Combine two error expressions into one.
+-- | Combine two expression errors into one.
data Error_Expr_Cons curr next
= Error_Expr_Curr curr
| Error_Expr_Next next
deriving (Eq, Show)
--- ** Class 'Error_Expr_LiftN'
--- | Construct the sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'
--- lifting a given error type to the top of a given error type stack.
-class Error_Expr_LiftN (n::Peano) err errs where
- error_expr_liftN :: Proxy n -> err -> errs
-instance Error_Expr_LiftN 'Zero curr curr where
- error_expr_liftN _ = id
-instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
- error_expr_liftN _ = Error_Expr_Curr
-instance
- Error_Expr_LiftN n other next =>
- Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
- error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)
+-- ** Type 'Error_Expr_Lift'
+-- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
+type Error_Expr_Lift err errs
+ = Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
--- | Lift an error type within a type stack to its top,
--- using a 'Peano' number calculated by 'Peano_of_Error_Expr'
--- to avoid the overlapping of the 'Error_Expr_LiftN' instances.
+-- | Convenient wrapper around 'error_expr_liftN',
+-- passing it the 'Peano' number from 'Peano_of_Error_Expr',
+-- used to avoid @OverlappingInstances@.
error_expr_lift
:: forall err errs.
Error_Expr_Lift err errs =>
err -> errs
error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
-type Error_Expr_Lift err errs
- = Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
+-- *** Type family 'Peano_of_Error_Expr'
-- | Return a 'Peano' number derived from the location
-- of a given error type within a given error type stack.
type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
Peano_of_Error_Expr err (Error_Expr_Cons err next) = 'Zero
Peano_of_Error_Expr other (Error_Expr_Cons curr next) = 'Succ (Peano_of_Error_Expr other next)
+-- *** Class 'Error_Expr_LiftN'
+-- | Lift a given expression to the top of a given expression stack including it,
+-- by constructing the appropriate sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'.
+class Error_Expr_LiftN (n::Peano) err errs where
+ error_expr_liftN :: Proxy n -> err -> errs
+instance Error_Expr_LiftN 'Zero curr curr where
+ error_expr_liftN _ = id
+instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
+ error_expr_liftN _ = Error_Expr_Curr
+instance
+ Error_Expr_LiftN n other next =>
+ Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
+ error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)
+
+-- ** Type 'Error_Expr_Unlift'
+-- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
+type Error_Expr_Unlift ex exs
+ = Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
+
+-- | Convenient wrapper around 'error_expr_unliftN',
+-- passing it the 'Peano' number from 'Peano_of_Error_Expr',
+-- used to avoid @OverlappingInstances@.
+error_expr_unlift
+ :: forall ex exs.
+ Error_Expr_Unlift ex exs =>
+ exs -> Maybe ex
+error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
+
+-- *** Class 'Error_Expr_UnliftN'
+-- | Try to unlift a given expression error out of a given expression error stack including it,
+-- by deconstructing the appropriate sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'.
+class Error_Expr_UnliftN (n::Peano) ex exs where
+ error_expr_unliftN :: Proxy n -> exs -> Maybe ex
+instance Error_Expr_UnliftN 'Zero curr curr where
+ error_expr_unliftN _ = Just
+instance Error_Expr_UnliftN 'Zero curr (Error_Expr_Cons curr next) where
+ error_expr_unliftN _ (Error_Expr_Curr x) = Just x
+ error_expr_unliftN _ (Error_Expr_Next _) = Nothing
+instance
+ Error_Expr_UnliftN n other next =>
+ Error_Expr_UnliftN ('Succ n) other (Error_Expr_Cons curr next) where
+ error_expr_unliftN _ (Error_Expr_Next x) = error_expr_unliftN (Proxy::Proxy n) x
+ error_expr_unliftN _ (Error_Expr_Curr _) = Nothing
+
-- ** Type 'Error_Expr_Read'
-data Error_Expr_Read ast
+-- | Common expression errors.
+data Error_Expr ast
= Error_Expr_Read Error_Read ast
+ | Error_Expr_Unsupported ast
deriving (Eq, Show)
-
-- * Class 'Sym_Int'
--- | Symantic for 'Int's.
+-- | Symantic.
class Sym_Int repr where
int :: Int -> repr Int
neg :: repr Int -> repr Int
add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
-- * Type 'Expr_Int'
--- | Expression's extension.
+-- | Expression.
data Expr_Int (root:: *)
type instance Root_of_Expr (Expr_Int root) = root
type instance Type_of_Expr (Expr_Int root) = Type_Int
( Type_Root_of_Expr root)
AST)
(Error_of_Expr AST root)
- , Error_Expr_Lift (Error_Expr_Read AST)
- (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr AST) (Error_of_Expr AST root)
, Type_Unlift Type_Int (Type_of_Expr root)
case asts of
[AST ast_int []] ->
case read_safe ast_int of
- Left err -> Left $ Just $ error_expr_lift
- (Error_Expr_Read err ast :: Error_Expr_Read AST)
+ Left err -> Left $ error_expr_lift $ Error_Expr_Read err ast
Right (i::Int) ->
k type_int $ Forall_Repr_with_Context $
const $ int i
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
AST "neg" asts -> unary_from asts neg
AST "add" asts -> binary_from asts add
- _ -> Left Nothing
+ _ -> Left $ error_expr_lift $ Error_Expr_Unsupported ast
where
unary_from asts
(op::forall repr. Sym_Int repr
case type_unlift $ unType_Root ty_x of
Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
k ty_x $ Forall_Repr_with_Context (op . x)
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_int)
(Exists_Type ty_x) ast
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 1 ast
binary_from asts
(op::forall repr. Sym_Int repr
Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_y) ->
k ty_x $ Forall_Repr_with_Context $
\c -> x c `op` y c
- Nothing -> Left $ Just $ error_lambda_lift $
+ Nothing -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_int)
(Exists_Type ty_y) ast
- Nothing -> Left $ Just $ error_lambda_lift $
+ Nothing -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_int)
(Exists_Type ty_x) ast
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 2 ast
error_lambda_lift
:: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
Expr_from ast (Expr_Lambda_Int lam)
=> Proxy lam
-> ast
- -> Either (Maybe (Error_of_Expr ast (Expr_Lambda_Int lam)))
+ -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
(Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
(Forall_Repr (Expr_Lambda_Int lam)))
expr_lambda_int_from _px_lam ast =
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
--- | Expression for /lambda abstraction/s.
+-- | Expression for /lambda abstraction/s
+-- in /Higher-Order Abstract Syntax/ (HOAS).
module Language.LOL.Symantic.Expr.Lambda where
import Data.Proxy (Proxy(..))
-- * Class 'Sym_Lambda'
--- | Symantic for /lambda abstraction/
--- in /higher-order abstract syntax/ (HOAS),
--- and with argument @arg@ and result @res@ of 'Lambda'
+-- | Symantic.
+--
+-- NOTE: argument @arg@ and result @res@ of 'Lambda'
-- wrapped inside 'lam': to control the calling
-- in the 'Repr_Host' instance.
--
-- | /Call-by-need/ lambda (aka. /lazyness/): lazy shares its argument, no matter what.
lazy :: (repr arg -> repr res) -> repr (Lambda lam arg res)
- default app :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res
+ default app :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res
default inline :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
default val :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
default lazy :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
lazy f = dup1 (lazy f) `Dup` dup2 (lazy f)
-- * Type 'Expr_Lambda'
--- | Expression's extension.
+-- | Expression.
data Expr_Lambda (lam:: * -> *) (root:: *)
type instance Root_of_Expr (Expr_Lambda lam root) = root
type instance Type_of_Expr (Expr_Lambda lam root) = Type_Fun lam
( Type_Root_of_Expr root)
AST)
(Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr AST) (Error_of_Expr AST root)
, Type_Unlift (Type_Fun lam) (Type_of_Expr root)
where
go
:: forall hs ret
- . Context (Var root) hs
+ . Context (Var (Type_Root_of_Expr root)) hs
-> ( forall h
. Type_Root_of_Expr root h
-> Forall_Repr_with_Context (Expr_Lambda lam root) hs h
- -> Either (Maybe (Error_of_Expr AST root)) ret )
- -> Either (Maybe (Error_of_Expr AST root)) ret
+ -> Either (Error_of_Expr AST root) ret )
+ -> Either (Error_of_Expr AST root) ret
go c k' =
case c of
- Context_Empty -> Left $ Just $ error_lambda_lift $
+ Context_Empty -> Left $ error_lambda_lift $
Error_Expr_Lambda_Var_unbound name ast
Var n ty `Context_Next` _ | n == name ->
k' ty $ Forall_Repr_with_Context $
go ctx' $ \ty (Forall_Repr_with_Context repr) ->
k' ty $ Forall_Repr_with_Context $
\(_ `Context_Next` c') -> repr c'
- _ -> Left $ Just $ error_lambda_lift $
+ _ -> Left $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 1 ast
AST "app" asts ->
case asts of
Just Refl ->
k ty_res $ Forall_Repr_with_Context $
\c -> lam c `app` arg_actual c
- Nothing -> Left $ Just $ error_lambda_lift $
+ Nothing -> Left $ error_lambda_lift $
Error_Expr_Fun_Argument_mismatch
(Exists_Type ty_arg_expected)
(Exists_Type ty_arg_actual) ast
- Nothing -> Left $ Just $ error_lambda_lift $
+ Nothing -> Left $ error_lambda_lift $
Error_Expr_Lambda_Not_a_lambda ast
- _ -> Left $ Just $ error_lambda_lift $
- Error_Expr_Type
- (error_type_lift $
- Error_Type_Fun_Wrong_number_of_arguments 2 ast
- ) ast
+ _ -> Left $ error_lambda_lift $
+ Error_Expr_Type (error_type_lift $
+ Error_Type_Fun_Wrong_number_of_arguments 2 ast) ast
AST "inline" asts -> lambda_from asts inline
AST "val" asts -> lambda_from asts val
AST "lazy" asts -> lambda_from asts lazy
- _ -> Left Nothing
+ -- AST "let_inline" asts -> let_from asts let_inline
+ _ -> Left $ error_expr_lift $ Error_Expr_Unsupported ast
where
lambda_from asts
(lam::forall repr arg res. Sym_Lambda lam repr
+ => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
+ case asts of
+ [AST name [], ast_ty_arg, ast_body] ->
+ case type_from
+ (Proxy::Proxy (Type_Root_of_Expr root))
+ ast_ty_arg
+ (Right . Exists_Type) of
+ Left err -> Left $ error_lambda_lift $ Error_Expr_Type err ast
+ Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) ->
+ expr_from (Proxy::Proxy root)
+ (Var name ty_arg `Context_Next` ctx) ast_body $
+ \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
+ k (ty_arg `type_fun` ty_res
+ :: Root_of_Type (Type_Root_of_Expr root)
+ (Lambda lam h_arg h_res)) $
+ Forall_Repr_with_Context $
+ \c -> lam $ \arg -> res (arg `Context_Next` c)
+ _ -> Left $ error_lambda_lift $
+ Error_Expr_Fun_Wrong_number_of_arguments 3 ast
+ {-let_from asts
+ (let_::forall repr arg res. Sym_Lambda lam repr
=> (repr arg -> repr res) -> repr (Lambda lam arg res)) =
case asts of
[AST name [], ast_ty_arg, ast_body] ->
:: Root_of_Type (Type_Root_of_Expr root)
(Lambda lam h_arg h_res)) $
Forall_Repr_with_Context $
- \c -> lam $ \arg -> res (arg `Context_Next` c)
+ \c -> let_ $ \arg -> res (arg `Context_Next` c)
_ -> Left $ Just $ error_lambda_lift $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
+ -}
error_lambda_lift
:: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
-> Error_of_Expr AST root
--
-- NOTE: this is a more verbose, less clear,
-- and maybe less efficient alternative
--- to maintaining the universal polymorphism of @repr@ at parsing time;
+-- to maintaining the universal polymorphism of @repr@ at parsing time
+-- as done with 'Forall_Repr_with_Context';
-- it is mainly here for the sake of curiosity.
module Language.LOL.Symantic.Repr.Dup where
-- when writting 'Trans' instances which
-- do not need to alterate those methods.
class Trans trans repr where
- -- | Lift a representation to the transformer's representation.
+ -- | Lift an interpreter to the transformer's.
trans_lift :: repr a -> trans repr a
- -- | Unlift a representation from the transformer's representation.
+ -- | Unlift an interpreter from the transformer's.
trans_apply :: trans repr a -> repr a
- -- | Convenient method to define the identity transformation for a unary function.
+ -- | Convenient method to define the identity transformation for a unary symantic method.
trans_map1 :: (repr a -> repr b) -> (trans repr a -> trans repr b)
trans_map1 f = trans_lift . f . trans_apply
- -- | Convenient method to define the identity transformation for a binary function.
+ -- | Convenient method to define the identity transformation for a binary symantic method.
trans_map2
:: (repr a -> repr b -> repr c)
-> (trans repr a -> trans repr b -> trans repr c)
x == y = isJust $ type_eq x y
instance -- Type_from AST
( Type_Root_Lift Type_Bool root
+ , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
+ -- NOTE: require UndecidableInstances.
, Error_Type_Lift (Error_Type_Fun AST) (Error_of_Type AST root)
-- NOTE: require UndecidableInstances.
) => Type_from AST (Type_Bool root) where
AST "Bool" asts ->
case asts of
[] -> k $ type_root_lift Type_Bool
- _ -> Left $ Just $ error_type_lift $
+ _ -> Left $ error_type_lift $
Error_Type_Fun_Wrong_number_of_arguments 0 ast
- _ -> Left Nothing
+ _ -> Left $ error_type_lift $ Error_Type_Unsupported ast
instance -- String_from_Type
String_from_Type (Type_Bool root) where
string_from_type Type_Bool = "Bool"
:: Proxy ty
-> ast
-> (forall h. Root_of_Type ty h
- -> Either (Maybe (Error_of_Type ast (Root_of_Type ty))) ret)
- -> Either (Maybe (Error_of_Type ast (Root_of_Type ty))) ret
+ -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
+ -> Either (Error_of_Type ast (Root_of_Type ty)) ret
-- ** Type family 'Root_of_Type'
-- | Return the root type of a type.
type instance Root_of_Type (Type_Root ty) = Type_Root ty
-- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
type instance Error_of_Type ast (Type_Root ty)
- = Error_of_Type ast (ty (Type_Root ty))
+ = Error_Type_Cons (Error_Type ast)
+ (Error_of_Type ast (ty (Type_Root ty)))
-- NOTE: require UndecidableInstances.
instance -- Type_Eq
Type_Eq (ty (Type_Root ty)) =>
, Type_from ast (next root)
, Root_of_Type (curr root) ~ root
, Root_of_Type (next root) ~ root
+ , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
) => Type_from ast (Type_Cons curr next root) where
type_from _px_ty ast k =
case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
Right ret -> ret
- Left Nothing -> type_from (Proxy::Proxy (next root)) ast k
- Left err -> Left err
+ Left err ->
+ case error_type_unlift err of
+ Just (Error_Type_Unsupported (_::ast)) -> type_from (Proxy::Proxy (next root)) ast k
+ _ -> Left err
instance -- String_from_Type
( String_from_Type (curr root)
, String_from_Type (next root)
type_liftN _ = Type_Next . type_liftN (Proxy::Proxy n)
-- | Convenient wrapper around 'type_liftN',
--- passing it the 'Peano' number from 'Peano_of_Type'.
+-- passing it the 'Peano' number from 'Peano_of_Type',
+-- used to avoid @OverlappingInstances@.
type_lift
:: forall ty tys (root:: * -> *) h.
Type_Lift ty tys =>
type_unliftN _ (Type_Curr _) = Nothing
-- | Convenient wrapper around 'type_unliftN',
--- passing it the 'Peano' number from 'Peano_of_Type'.
+-- passing it the 'Peano' number from 'Peano_of_Type',
+-- used to avoid @OverlappingInstances@.
type_unlift
:: forall ty tys (root:: * -> *) h.
Type_Unlift ty tys =>
error_type_liftN _ = Error_Type_Next . error_type_liftN (Proxy::Proxy n)
-- | Convenient wrapper around 'error_type_unliftN',
--- passing it the 'Peano' number from 'Peano_of_Type'.
+-- passing it the 'Peano' number from 'Peano_of_Type',
+-- used to avoid @OverlappingInstances@.
error_type_lift
:: forall err errs.
Error_Type_Lift err errs =>
err -> errs
error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
+-- ** Type 'Error_Type_Unlift'
+-- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
+type Error_Type_Unlift ty tys
+ = Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
+
+-- | Convenient wrapper around 'error_type_unliftN',
+-- passing it the 'Peano' number from 'Peano_of_Error_Type',
+-- used to avoid @OverlappingInstances@.
+error_type_unlift
+ :: forall ty tys.
+ Error_Type_Unlift ty tys =>
+ tys -> Maybe ty
+error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
+
+-- *** Class 'Error_Type_UnliftN'
+-- | Try to unlift a given type error out of a given type error stack including it,
+-- by deconstructing the appropriate sequence of 'Error_Type_Curr' and 'Error_Type_Next'.
+class Error_Type_UnliftN (n::Peano) ty tys where
+ error_type_unliftN :: Proxy n -> tys -> Maybe ty
+instance Error_Type_UnliftN 'Zero curr curr where
+ error_type_unliftN _ = Just
+instance Error_Type_UnliftN 'Zero curr (Error_Type_Cons curr next) where
+ error_type_unliftN _ (Error_Type_Curr x) = Just x
+ error_type_unliftN _ (Error_Type_Next _) = Nothing
+instance
+ Error_Type_UnliftN n other next =>
+ Error_Type_UnliftN ('Succ n) other (Error_Type_Cons curr next) where
+ error_type_unliftN _ (Error_Type_Next x) = error_type_unliftN (Proxy::Proxy n) x
+ error_type_unliftN _ (Error_Type_Curr _) = Nothing
+
+-- ** Type 'Error_Type_Read'
+-- | Common type errors.
+data Error_Type ast
+ = Error_Type_Unsupported ast
+ deriving (Eq, Show)
+
-- * Class 'String_from_Type'
-- | Return a 'String' from a type.
class String_from_Type ty where
( Type_Eq root
, Type_from AST root
, Type_Root_Lift (Type_Fun lam) root
+ , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
+ -- NOTE: require UndecidableInstances.
, Error_Type_Lift (Error_Type_Fun AST) (Error_of_Type AST root)
-- NOTE: require UndecidableInstances.
, Root_of_Type root ~ root
type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
k (type_root_lift $ ty_arg `Type_Fun` ty_res
:: root (Lambda lam h_arg h_res))
- _ -> Left $ Just $ error_type_lift $
+ _ -> Left $ error_type_lift $
Error_Type_Fun_Wrong_number_of_arguments 2 ast
- type_from _px_ty _ast _k = Left Nothing
+ type_from _px_ty ast _k = Left $ error_type_lift $ Error_Type_Unsupported ast
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Fun lam root) where
x == y = isJust $ type_eq x y
instance -- Type_from AST
( Type_Root_Lift Type_Int root
+ , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
+ -- NOTE: require UndecidableInstances.
, Error_Type_Lift (Error_Type_Fun AST) (Error_of_Type AST root)
-- NOTE: require UndecidableInstances.
) => Type_from AST (Type_Int root) where
AST "Int" asts ->
case asts of
[] -> k $ type_root_lift Type_Int
- _ -> Left $ Just $ error_type_lift $
+ _ -> Left $ error_type_lift $
Error_Type_Fun_Wrong_number_of_arguments 0 ast
- _ -> Left Nothing
+ _ -> Left $ error_type_lift $ Error_Type_Unsupported ast
instance -- String_from_Type
String_from_Type (Type_Int root) where
string_from_type Type_Int = "Int"
==> Right (type_bool :: Type_Fun_Bool lam Bool) $
(Proxy :: Proxy (Type_Fun_Bool lam))
, AST "->" [AST "Bool" []]
- ==> Left (Just $ error_type_lift $
+ ==> Left (error_type_lift $
Error_Type_Fun_Wrong_number_of_arguments 2 (AST "->" [AST "Bool" []])) $
(Proxy :: Proxy (Type_Fun_Bool lam))
, AST "->" [AST "Bool" [], AST "Bool" []]
:: Type_Fun_Bool lam (lam Bool -> lam (lam Bool -> lam Bool))) $
(Proxy :: Proxy (Type_Fun_Bool lam))
, AST "Int" []
- ==> Left Nothing $
+ ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
(Proxy :: Proxy (Type_Fun_Bool lam))
, AST "->" [AST "Bool" [], AST "Int" []]
- ==> Left Nothing $
+ ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
(Proxy :: Proxy (Type_Fun_Bool lam))
, AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
, AST "Int" [] ]
- ==> Left Nothing $
+ ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
(Proxy :: Proxy (Type_Fun_Bool lam))
]
, testGroup "Int"
==> Right (type_int :: Type_Fun_Int lam Int) $
(Proxy :: Proxy (Type_Fun_Int lam))
, AST "->" [AST "Int" []]
- ==> Left (Just $ error_type_lift $
+ ==> Left (error_type_lift $
Error_Type_Fun_Wrong_number_of_arguments 2 (AST "->" [AST "Int" []])) $
(Proxy :: Proxy (Type_Fun_Int lam))
, AST "->" [AST "Int" [], AST "Int" []]
:: Type_Fun_Int lam (lam Int -> lam (lam Int -> lam Int))) $
(Proxy :: Proxy (Type_Fun_Int lam))
, AST "Bool" []
- ==> Left Nothing $
+ ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
(Proxy :: Proxy (Type_Fun_Int lam))
, AST "->" [AST "Int" [], AST "Bool" []]
- ==> Left Nothing $
+ ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
(Proxy :: Proxy (Type_Fun_Int lam))
, AST "->" [ AST "->" [AST "Bool" [], AST "Int" []]
, AST "Bool" [] ]
- ==> Left Nothing $
+ ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
(Proxy :: Proxy (Type_Fun_Int lam))
]
]
sourcephile / git / haskell / symantic.git / commitdiff