( ty ~ Type_Root_of_Expr ex
, root ~ Root_of_Expr ex
, ast ~ AST
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
( ty ~ Type_Root_of_Expr ex
, root ~ Root_of_Expr ex
, ast ~ AST
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
Error_Type_Wrong_number_of_arguments ast 0
_ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Fun
- ( Type_Eq root
+ ( Eq_Type root
, Type_from AST root
, Type_Root_Lift (Type_Fun lam) root
, Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
Error_Type_Wrong_number_of_arguments ast 2
_ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Maybe
- ( Type_Eq root
+ ( Eq_Type root
, Type_from AST root
, Type_Root_Lift Type_Maybe root
, Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
) => Expr_from AST (Expr_Maybe lam root) where
expr_from ex ast ctx k =
case ast of
- AST "maybe" asts -> from_ast3 asts maybe_from ex ast ctx k
+ AST "maybe" asts -> from_ast3 asts maybe_from ex ast ctx k
AST "nothing" asts -> from_ast1 asts nothing_from ex ast ctx k
- AST "just" asts -> from_ast1 asts just_from ex ast ctx k
+ AST "just" asts -> from_ast1 asts just_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Eq
( Type_from AST (Type_Root_of_Expr root)
, Type_Lift Type_Bool (Type_of_Expr root)
- , Type_Constraint Eq (Type_Root_of_Expr root)
+ , Constraint_Type Eq (Type_Root_of_Expr root)
, Expr_from AST root
, Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
, Root_of_Expr root ~ root
instance -- Expr_from AST Expr_Ord
( Type_from AST (Type_Root_of_Expr root)
, Type_Lift Type_Ordering (Type_of_Expr root)
- , Type_Constraint Ord (Type_Root_of_Expr root)
+ , Constraint_Type Ord (Type_Root_of_Expr root)
, Expr_from AST root
, Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
, Root_of_Expr root ~ root
) => Expr_from AST (Expr_List lam root) where
expr_from ex ast ctx k =
case ast of
- AST "[]" asts -> from_ast1 asts list_empty_from ex ast ctx k
- AST ":" asts -> from_ast2 asts list_cons_from ex ast ctx k
+ AST "[]" asts -> from_ast1 asts list_empty_from ex ast ctx k
+ AST ":" asts -> from_ast2 asts list_cons_from ex ast ctx k
AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Map
, Expr_from AST root
, Type_Lift (Type_Fun lam) (Type_of_Expr root)
, Type_Unlift (Type_Fun lam) (Type_of_Expr root)
- , Type_Lift Type_Map (Type_of_Expr root)
- , Type_Unlift Type_Map (Type_of_Expr root)
- , Type_Lift Type_List (Type_of_Expr root)
- , Type_Unlift Type_List (Type_of_Expr root)
- , Type_Lift Type_Tuple2 (Type_of_Expr root)
- , Type_Unlift Type_Tuple2 (Type_of_Expr root)
- , Type_Constraint Ord (Type_Root_of_Expr root)
+ , Type_Lift Type_Map (Type_of_Expr root)
+ , Type_Unlift Type_Map (Type_of_Expr root)
+ , Type_Lift Type_List (Type_of_Expr root)
+ , Type_Unlift Type_List (Type_of_Expr root)
+ , Type_Lift Type_Tuple2 (Type_of_Expr root)
+ , Type_Unlift Type_Tuple2 (Type_of_Expr root)
+ , Constraint_Type Ord (Type_Root_of_Expr root)
, Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
, Root_of_Expr root ~ root
, Implicit_HBool (Is_Last_Expr (Expr_Map lam root) root)
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
- case ty `type_eq` ty_expected of
+ case ty `eq_type` ty_expected of
Nothing -> return $ Left $
error_expr (Proxy::Proxy (Ex IO)) $
Error_Expr_Type_mismatch ast
:: forall root ty lit ex ast hs ret.
( ty ~ Type_Root_of_Expr ex
, root ~ Root_of_Expr ex
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
op1_from op ty_lit ast_x ex ast ctx k =
expr_from (Proxy::Proxy root) ast_x ctx $
\ty_x (Forall_Repr_with_Context x) ->
- check_type_eq ex ast ty_lit ty_x $ \Refl ->
+ check_eq_type ex ast ty_lit ty_x $ \Refl ->
k ty_x $ Forall_Repr_with_Context (op . x)
-- | Parse a binary operator.
:: forall root ty lit ex ast hs ret.
( ty ~ Type_Root_of_Expr ex
, root ~ Root_of_Expr ex
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
op2_from op ty_lit ast_x ast_y ex ast ctx k =
expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
- check_type_eq ex ast ty_lit ty_x $ \Refl ->
- check_type_eq ex ast ty_lit ty_y $ \Refl ->
+ check_eq_type ex ast ty_lit ty_x $ \Refl ->
+ check_eq_type ex ast ty_lit ty_y $ \Refl ->
k ty_x $ Forall_Repr_with_Context $
\c -> x c `op` y c
-- | Parsing utility to check that two types are equal,
-- or raise 'Error_Expr_Type_mismatch'.
-check_type_eq
+check_eq_type
:: forall ast ex root ty x y ret.
( root ~ Root_of_Expr ex
, ty ~ Type_Root_of_Expr ex
- , Type_Eq ty
+ , Eq_Type ty
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
)
=> Proxy ex -> ast -> ty x -> ty y
-> (x :~: y -> Either (Error_of_Expr ast root) ret)
-> Either (Error_of_Expr ast root) ret
-check_type_eq ex ast x y k =
- case x `type_eq` y of
+check_eq_type ex ast x y k =
+ case x `eq_type` y of
Just Refl -> k Refl
Nothing -> Left $ error_expr ex $
Error_Expr_Type_mismatch ast
-- | Parsing utility to check that a type is has instance of a given 'Constraint',
-- or raise 'Error_Expr_Constraint_missing'.
-check_type_constraint
+check_constraint_type
:: forall ast ex c root ty h ret.
( root ~ Root_of_Expr ex
, ty ~ Type_Root_of_Expr ex
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
- , Type_Constraint c ty
+ , Constraint_Type c ty
)
=> Proxy ex -> Proxy c -> ast -> ty h
-> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
-> Either (Error_of_Expr ast root) ret
-check_type_constraint ex c ast ty k =
- case type_constraint c ty of
+check_constraint_type ex c ast ty k =
+ case constraint_type c ty of
Just Dict -> k Dict
Nothing -> Left $ error_expr ex $
Error_Expr_Constraint_missing ast
:: forall root ty ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Eq root)
, Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
, Root_of_Expr root ~ root
- , Type_Constraint Eq ty
+ , Constraint_Type Eq ty
) => ast -> ast
-> Expr_From ast (Expr_Eq root) hs ret
eq_from ast_x ast_y ex ast ctx k =
\(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
expr_from (Proxy::Proxy root) ast_y ctx $
\(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
- check_type_eq ex ast ty_x ty_y $ \Refl ->
- check_type_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
+ check_eq_type ex ast ty_x ty_y $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
k type_bool $ Forall_Repr_with_Context $
\c -> x c == y c
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
- case ty `type_eq` ty_expected of
+ case ty `eq_type` ty_expected of
Nothing -> return $ Left $
error_expr (Proxy::Proxy (Ex IO)) $
Error_Expr_Type_mismatch ast
if_from
:: forall root ty ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_If root)
- , Type_Eq ty
+ , Eq_Type ty
, Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
\(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
expr_from (Proxy::Proxy root) ast_ko ctx $
\(ty_ko::Type_Root_of_Expr root h_ko) (Forall_Repr_with_Context ko) ->
- check_type_eq ex ast type_bool ty_cond $ \Refl ->
- check_type_eq ex ast ty_ok ty_ko $ \Refl ->
+ check_eq_type ex ast type_bool ty_cond $ \Refl ->
+ check_eq_type ex ast ty_ok ty_ko $ \Refl ->
k ty_ok $ Forall_Repr_with_Context $
\c -> if_ (cond c) (ok c) (ko c)
when_from
:: forall root ty ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_When root)
- , Type_Eq ty
+ , Eq_Type ty
, Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
, Type_Root_Lift Type_Unit (Type_Root_of_Expr root)
, Expr_from ast root
\(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
expr_from (Proxy::Proxy root) ast_ok ctx $
\(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
- check_type_eq ex ast type_bool ty_cond $ \Refl ->
- check_type_eq ex ast type_unit ty_ok $ \Refl ->
+ check_eq_type ex ast type_bool ty_cond $ \Refl ->
+ check_eq_type ex ast type_unit ty_ok $ \Refl ->
k ty_ok $ Forall_Repr_with_Context $
\c -> when (cond c) (ok c)
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
- case ty `type_eq` ty_expected of
+ case ty `eq_type` ty_expected of
Nothing -> return $ Left $
error_expr (Proxy::Proxy (Ex IO)) $
Error_Expr_Type_mismatch ast
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
- case ty `type_eq` ty_expected of
+ case ty `eq_type` ty_expected of
Nothing -> return $ Left $
error_expr (Proxy::Proxy (Ex IO)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty_lam)
Just (ty_arg_expected `Type_Fun` ty_res
:: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
- check_type_eq ex ast
+ check_eq_type ex ast
ty_arg_expected ty_arg_actual $ \Refl ->
k ty_res $ Forall_Repr_with_Context $
\c -> lam c `app` arg_actual c
import Language.Symantic.Trans.Common
import Language.Symantic.Expr.Common
import Language.Symantic.Expr.Lambda
-import Language.Symantic.Expr.Bool
-- * Class 'Sym_List_Lam'
-- | Symantic.
list_cons_from
:: forall root lam ty ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_List lam root)
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Type_Lift Type_List (Type_of_Expr root)
, Type_Unlift Type_List (Type_of_Expr root)
expr_from (Proxy::Proxy root) ast_l ctx $
\(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
check_type_list ex ast ty_l $ \(Type_List ty_l_a) ->
- check_type_eq ex ast ty_a ty_l_a $ \Refl ->
+ check_eq_type ex ast ty_a ty_l_a $ \Refl ->
k (type_list ty_a) $ Forall_Repr_with_Context $
\c -> list_cons (a c) (l c)
+-- | Parse 'list'.
+list_from
+ :: forall root lam ex ty ty_root ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_List lam root)
+ , ty_root ~ Type_Root_of_Expr root
+ , ex ~ Expr_List lam root
+ , Eq_Type (Type_Root_of_Expr root)
+ , Type_from ast ty_root
+ , Expr_from ast root
+ , Type_Lift Type_List (Type_of_Expr root)
+ , Type_Unlift Type_List (Type_of_Expr root)
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ , Root_of_Type ty_root ~ ty_root
+ ) => ast -> [ast]
+ -> Expr_From ast ex hs ret
+list_from ast_ty_a ast_as =
+ case type_from (Proxy::Proxy ty_root)
+ ast_ty_a (Right . Exists_Type) of
+ Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
+ Right (Exists_Type ty_a) -> go ty_a [] ast_as
+ where
+ go :: Type_Root_of_Expr root ty_a
+ -> [Forall_Repr_with_Context root hs ty_a]
+ -> [ast]
+ -> Expr_From ast (Expr_List lam root) hs ret
+ go ty_a as [] _ex _ast _ctx k =
+ k (type_list ty_a) $ Forall_Repr_with_Context $
+ \c -> list ((\(Forall_Repr_with_Context a) -> a c) <$> as)
+ go ty_a as (ast_x:ast_xs) ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_x ctx $
+ \(ty_x::Type_Root_of_Expr root h_x) x ->
+ check_eq_type ex ast ty_a ty_x $ \Refl ->
+ go ty_a (x:as) ast_xs ex ast ctx k
+
-- | Parse 'list_filter'.
list_filter_from
:: forall root lam ty ty_root ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_List lam root)
, ty_root ~ Type_of_Expr root
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Type_Lift Type_Bool ty_root
, Type_Lift (Type_Fun lam) ty_root
\(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
check_type_fun ex ast ty_f $ \(ty_f_a `Type_Fun` ty_f_b
:: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
- check_type_eq ex ast type_bool ty_f_b $ \Refl ->
+ check_eq_type ex ast type_bool ty_f_b $ \Refl ->
check_type_list ex ast ty_l $ \(Type_List ty_l_a) ->
- check_type_eq ex ast ty_f_a ty_l_a $ \Refl ->
+ check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
k ty_l $ Forall_Repr_with_Context $
\c -> list_filter (f c) (l c)
-
--- ** Type 'Expr_Lambda_List_Bool'
--- | Convenient alias.
-type Expr_Lambda_List_Bool lam
- = Expr_Root (Expr_Lambda lam .|. Expr_List lam .|. Expr_Bool)
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_list_bool_from
- :: forall lam ast root.
- ( Expr_from ast (Expr_Lambda_List_Bool lam)
- , root ~ Expr_Lambda_List_Bool lam
- ) => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast root)
- (Exists_Type_and_Repr (Type_Root_of_Expr root)
- (Forall_Repr root))
-expr_lambda_list_bool_from _lam ast =
- expr_from (Proxy::Proxy root) ast
- Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
- Right $ Exists_Type_and_Repr ty $
- Forall_Repr $ repr Context_Empty
module Expr.List.Test where
import Test.Tasty
+{-
import Test.Tasty.HUnit
import Control.Arrow (left)
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
+-}
import Prelude hiding (mod, (==))
import Language.Symantic.Repr
-- * Tests
(==>) ast expected =
testCase (show ast) $
- case expr_lambda_maybe_bool_from (Proxy::Proxy IO) ast of
+ case ex_from (Proxy::Proxy IO) ast of
Left err -> Left err @?= snd `left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
- Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_List_Bool IO) h, _::h, _::Text) ->
+ Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
- case ty `type_eq` ty_expected of
+ case ty `eq_type` ty_expected of
Nothing -> return $ Left $
- error_expr (Proxy::Proxy (Expr_Lambda_List_Bool IO)) $
+ error_expr (Proxy::Proxy (Ex IO)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
, Type_Lift Type_Map ty_root
, Type_Lift Type_Tuple2 ty_root
, Type_Unlift Type_Tuple2 ty_root
- , Type_Constraint Ord ty
+ , Constraint_Type Ord ty
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
, Root_of_Expr root ~ root
\(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
check_type_list ex ast ty_l $ \(Type_List ty_l_t) ->
check_type_tuple2 ex ast ty_l_t $ \(Type_Tuple2 ty_k ty_a) ->
- check_type_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
\c -> map_from_list (l c)
:: forall root lam ty ty_root ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Map lam root)
, ty_root ~ Type_of_Expr root
- , Type_Eq ty
+ , Eq_Type ty
, Expr_from ast root
, Type_Lift (Type_Fun lam) ty_root
, Type_Unlift (Type_Fun lam) ty_root
, Type_Lift Type_Map ty_root
, Type_Unlift Type_Map ty_root
- , Type_Constraint Ord ty
+ , Constraint_Type Ord ty
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
, Root_of_Expr root ~ root
check_type_fun ex ast ty_f $ \(ty_f_a `Type_Fun` ty_f_b
:: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
check_type_map ex ast ty_m $ \(Type_Map ty_m_k ty_m_a) ->
- check_type_eq ex ast ty_f_a ty_m_a $ \Refl ->
- check_type_constraint ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
+ check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
\c -> map_map (f c) (m c)
:: forall root lam ty ty_root ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
, ty_root ~ Type_of_Expr root
- , Type_Eq ty
+ , Eq_Type ty
, Expr_from ast root
, Type_Lift (Type_Fun lam) ty_root
, Type_Unlift (Type_Fun lam) ty_root
check_type_fun ex ast ty_j $ \(ty_j_a `Type_Fun` ty_j_b
:: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
check_type_maybe ex ast ty_m $ \(Type_Maybe ty_m_a) ->
- check_type_eq ex ast ty_n ty_j_b $ \Refl ->
- check_type_eq ex ast ty_m_a ty_j_a $ \Refl ->
+ check_eq_type ex ast ty_n ty_j_b $ \Refl ->
+ check_eq_type ex ast ty_m_a ty_j_a $ \Refl ->
k ty_n $ Forall_Repr_with_Context $
\c -> maybe (n c) (j c) (m c)
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
- case ty `type_eq` ty_expected of
+ case ty `eq_type` ty_expected of
Nothing -> return $ Left $
error_expr (Proxy::Proxy (Ex IO)) $
Error_Expr_Type_mismatch ast
:: forall root ty ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Ord root)
, Type_Root_Lift Type_Ordering (Type_Root_of_Expr root)
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
, Root_of_Expr root ~ root
- , Type_Constraint Ord ty
+ , Constraint_Type Ord ty
) => ast -> ast
-> Expr_From ast (Expr_Ord root) hs ret
compare_from ast_x ast_y ex ast ctx k =
\(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
expr_from (Proxy::Proxy root) ast_y ctx $
\(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
- check_type_eq ex ast ty_x ty_y $ \Refl ->
- check_type_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
+ check_eq_type ex ast ty_x ty_y $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
k type_ordering $ Forall_Repr_with_Context $
\c -> x c `compare` y c
tuple2_from
:: forall root lam ty ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Tuple2 lam root)
- , Type_Eq (Type_Root_of_Expr root)
+ , Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Type_Lift Type_Tuple2 (Type_of_Expr root)
, Type_Unlift Type_Tuple2 (Type_of_Expr root)
import qualified Expr.Maybe.Test as Maybe.Test
import qualified Expr.Eq.Test as Eq.Test
import qualified Expr.If.Test as If.Test
+import qualified Expr.List.Test as List.Test
tests :: TestTree
tests = testGroup "Text" $
[ If.Test.e1 ==> "if True then False else True"
, If.Test.e2 ==> "if True && True then False else True"
]
+ , testGroup "List"
+ [ List.Test.e1 ==> "list_filter (\\!x0 -> if x0 % 2 == 0 then True else False):[1, 2, 3, 4, 5]"
+ ]
]
type instance Root_of_Type (Type_Bool root) = root
type instance Error_of_Type ast (Type_Bool root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq (Type_Bool root) where
- type_eq Type_Bool Type_Bool = Just Refl
+instance -- Eq_Type
+ Eq_Type (Type_Bool root) where
+ eq_type Type_Bool Type_Bool = Just Refl
instance -- Eq
Eq (Type_Bool root h) where
- x == y = isJust $ x `type_eq` y
+ x == y = isJust $ x `eq_type` y
instance -- String_from_Type
String_from_Type (Type_Bool root) where
string_from_type Type_Bool = "Bool"
instance -- Show
Show (Type_Bool root h) where
show = string_from_type
-instance Type_Constraint Eq (Type_Bool root) where
- type_constraint _c Type_Bool = Just Dict
-instance Type_Constraint Ord (Type_Bool root) where
- type_constraint _c Type_Bool = Just Dict
+instance Constraint_Type Eq (Type_Bool root) where
+ constraint_type _c Type_Bool = Just Dict
+instance Constraint_Type Ord (Type_Bool root) where
+ constraint_type _c Type_Bool = Just Dict
-- | Convenient alias to include a 'Type_Bool' within a type.
type_bool :: Type_Root_Lift Type_Bool root => root Bool
import Language.Symantic.Lib.Data.Peano
import GHC.Prim (Constraint)
--- * Class 'Type_Eq'
+-- * Class 'Eq_Type'
-- | Test two types for equality,
-- returning an Haskell type-level proof
-- of the equality when it holds.
-class Type_Eq (ty:: * -> *) where
- type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
+class Eq_Type (ty:: * -> *) where
+ eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
--- * Class 'Type_Constraint'
+-- * Class 'Constraint_Type'
-- | Test if a type satisfies a given 'Constraint',
-- returning an Haskell type-level proof
-- of that satisfaction when it holds.
-class Type_Constraint (c:: * -> Constraint) (ty:: * -> *) where
- type_constraint :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
- type_constraint _c _ = Nothing
+class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
+ constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
+ constraint_type _c _ = Nothing
-- ** Type 'Dict'
-- | 'Dict' captures the dictionary of a 'Constraint':
-- * Class 'Type_from'
-- | Parse given @ast@ into a 'Root_of_Type',
-- or return an 'Error_of_Type'.
-class Type_Eq ty =>
+class Eq_Type ty =>
Type_from ast (ty:: * -> *) where
type_from
:: Proxy ty
type instance Error_of_Type ast (Type_Root ty)
= Error_Type_Alt (Error_Type ast)
(Error_of_Type ast (ty (Type_Root ty)))
-instance -- Type_Eq
- Type_Eq (ty (Type_Root ty)) =>
- Type_Eq (Type_Root ty) where
- type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
+instance -- Eq_Type
+ Eq_Type (ty (Type_Root ty)) =>
+ Eq_Type (Type_Root ty) where
+ eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
instance -- Eq
- Type_Eq (Type_Root ty) =>
+ Eq_Type (Type_Root ty) =>
Eq (Type_Root ty h) where
- x == y = isJust $ x `type_eq` y
-instance -- Type_Constraint c Type_Root
- Type_Constraint c (ty (Type_Root ty)) =>
- Type_Constraint c (Type_Root ty) where
- type_constraint c (Type_Root ty) = type_constraint c ty
+ x == y = isJust $ x `eq_type` y
+instance -- Constraint_Type c Type_Root
+ Constraint_Type c (ty (Type_Root ty)) =>
+ Constraint_Type c (Type_Root ty) where
+ constraint_type c (Type_Root ty) = constraint_type c ty
instance -- Type_from
- ( Type_Eq (Type_Root ty)
+ ( Eq_Type (Type_Root ty)
, Type_from ast (ty (Type_Root ty))
, Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
) => Type_from ast (Type_Root ty) where
= No_Error_Type
deriving (Eq, Show)
-instance -- Type_Eq
- ( Type_Eq (curr root)
- , Type_Eq (next root)
- ) => Type_Eq (Type_Alt curr next root) where
- type_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type_eq` y
- type_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type_eq` y
- type_eq _ _ = Nothing
+instance -- Eq_Type
+ ( Eq_Type (curr root)
+ , Eq_Type (next root)
+ ) => Eq_Type (Type_Alt curr next root) where
+ eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
+ eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
+ eq_type _ _ = Nothing
instance -- Eq
- ( Type_Eq (curr root)
- , Type_Eq (next root)
+ ( Eq_Type (curr root)
+ , Eq_Type (next root)
) => Eq (Type_Alt curr next root h) where
- x == y = isJust $ x `type_eq` y
-instance -- Type_Constraint c Type_Alt
- ( Type_Constraint c (curr root)
- , Type_Constraint c (next root)
- ) => Type_Constraint c (Type_Alt curr next root) where
- type_constraint c (Type_Alt_Curr ty) = type_constraint c ty
- type_constraint c (Type_Alt_Next ty) = type_constraint c ty
+ x == y = isJust $ x `eq_type` y
+instance -- Constraint_Type c Type_Alt
+ ( Constraint_Type c (curr root)
+ , Constraint_Type c (next root)
+ ) => Constraint_Type c (Type_Alt curr next root) where
+ constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
+ constraint_type c (Type_Alt_Next ty) = constraint_type c ty
instance -- Type_from
- ( Type_Eq (curr root)
+ ( Eq_Type (curr root)
, Type_from ast (curr root)
, Type_from ast (next root)
, Root_of_Type (curr root) ~ root
data Exists_Type ty
= forall h. Exists_Type (ty h)
instance -- Eq
- Type_Eq ty =>
+ Eq_Type ty =>
Eq (Exists_Type ty) where
Exists_Type xh == Exists_Type yh =
- isJust $ xh `type_eq` yh
+ isJust $ xh `eq_type` yh
instance -- Show
String_from_Type ty =>
Show (Exists_Type ty) where
type instance Root_of_Type (Type_Fun lam root) = root
type instance Error_of_Type ast (Type_Fun lam root) = ()
-instance -- Type_Eq
- Type_Eq root =>
- Type_Eq (Type_Fun lam root) where
- type_eq
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Fun lam root) where
+ eq_type
(arg1 `Type_Fun` res1)
(arg2 `Type_Fun` res2)
- | Just Refl <- arg1 `type_eq` arg2
- , Just Refl <- res1 `type_eq` res2
+ | Just Refl <- arg1 `eq_type` arg2
+ , Just Refl <- res1 `eq_type` res2
= Just Refl
- type_eq _ _ = Nothing
+ eq_type _ _ = Nothing
instance -- Eq
- Type_Eq root =>
+ Eq_Type root =>
Eq (Type_Fun lam root h) where
- x == y = isJust $ x `type_eq` y
+ x == y = isJust $ x `eq_type` y
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Fun lam root) where
String_from_Type root =>
Show (Type_Fun lam root h) where
show = string_from_type
-instance Type_Constraint Eq (Type_Fun lam root)
-instance Type_Constraint Ord (Type_Fun lam root)
+instance Constraint_Type Eq (Type_Fun lam root)
+instance Constraint_Type Ord (Type_Fun lam root)
type_fun_from
:: forall (lam :: * -> *) (root :: * -> *) ast ret.
type instance Root_of_Type (Type_Int root) = root
type instance Error_of_Type ast (Type_Int root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq (Type_Int root) where
- type_eq Type_Int Type_Int = Just Refl
+instance -- Eq_Type
+ Eq_Type (Type_Int root) where
+ eq_type Type_Int Type_Int = Just Refl
instance -- Eq
Eq (Type_Int root h) where
- x == y = isJust $ x `type_eq` y
+ x == y = isJust $ x `eq_type` y
instance -- String_from_Type
String_from_Type (Type_Int root) where
string_from_type Type_Int = "Int"
instance -- Show
Show (Type_Int root h) where
show = string_from_type
-instance Type_Constraint Eq (Type_Int root) where
- type_constraint _c Type_Int = Just Dict
-instance Type_Constraint Ord (Type_Int root) where
- type_constraint _c Type_Int = Just Dict
+instance Constraint_Type Eq (Type_Int root) where
+ constraint_type _c Type_Int = Just Dict
+instance Constraint_Type Ord (Type_Int root) where
+ constraint_type _c Type_Int = Just Dict
-- | Convenient alias to include a 'Type_Int' within a type.
type_int :: Type_Root_Lift Type_Int root => root Int
type instance Root_of_Type (Type_List root) = root
type instance Error_of_Type ast (Type_List root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq root =>
- Type_Eq (Type_List root) where
- type_eq (Type_List a1) (Type_List a2)
- | Just Refl <- a1 `type_eq` a2
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_List root) where
+ eq_type (Type_List a1) (Type_List a2)
+ | Just Refl <- a1 `eq_type` a2
= Just Refl
- type_eq _ _ = Nothing
+ eq_type _ _ = Nothing
instance -- Eq
- Type_Eq root =>
+ Eq_Type root =>
Eq (Type_List root h) where
- x == y = isJust $ type_eq x y
+ x == y = isJust $ eq_type x y
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_List root) where
type instance Root_of_Type (Type_Map root) = root
type instance Error_of_Type ast (Type_Map root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq root =>
- Type_Eq (Type_Map root) where
- type_eq (Type_Map k1 a1) (Type_Map k2 a2)
- | Just Refl <- k1 `type_eq` k2
- , Just Refl <- a1 `type_eq` a2
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Map root) where
+ eq_type (Type_Map k1 a1) (Type_Map k2 a2)
+ | Just Refl <- k1 `eq_type` k2
+ , Just Refl <- a1 `eq_type` a2
= Just Refl
- type_eq _ _ = Nothing
+ eq_type _ _ = Nothing
instance -- Eq
- Type_Eq root =>
+ Eq_Type root =>
Eq (Type_Map root h) where
- x == y = isJust $ type_eq x y
+ x == y = isJust $ eq_type x y
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Map root) where
type instance Root_of_Type (Type_Maybe root) = root
type instance Error_of_Type ast (Type_Maybe root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq root =>
- Type_Eq (Type_Maybe root) where
- type_eq (Type_Maybe a1) (Type_Maybe a2)
- | Just Refl <- a1 `type_eq` a2
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Maybe root) where
+ eq_type (Type_Maybe a1) (Type_Maybe a2)
+ | Just Refl <- a1 `eq_type` a2
= Just Refl
- type_eq _ _ = Nothing
+ eq_type _ _ = Nothing
instance -- Eq
- Type_Eq root =>
+ Eq_Type root =>
Eq (Type_Maybe root h) where
- x == y = isJust $ type_eq x y
+ x == y = isJust $ eq_type x y
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Maybe root) where
type instance Root_of_Type (Type_Ordering root) = root
type instance Error_of_Type ast (Type_Ordering root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq (Type_Ordering root) where
- type_eq Type_Ordering Type_Ordering = Just Refl
+instance -- Eq_Type
+ Eq_Type (Type_Ordering root) where
+ eq_type Type_Ordering Type_Ordering = Just Refl
instance -- Eq
Eq (Type_Ordering root h) where
- x == y = isJust $ x `type_eq` y
+ x == y = isJust $ x `eq_type` y
instance -- String_from_Type
String_from_Type (Type_Ordering root) where
string_from_type Type_Ordering = "Ordering"
type instance Root_of_Type (Type_Tuple2 root) = root
type instance Error_of_Type ast (Type_Tuple2 root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq root =>
- Type_Eq (Type_Tuple2 root) where
- type_eq (Type_Tuple2 a1 b1) (Type_Tuple2 a2 b2)
- | Just Refl <- a1 `type_eq` a2
- , Just Refl <- b1 `type_eq` b2
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Tuple2 root) where
+ eq_type (Type_Tuple2 a1 b1) (Type_Tuple2 a2 b2)
+ | Just Refl <- a1 `eq_type` a2
+ , Just Refl <- b1 `eq_type` b2
= Just Refl
- type_eq _ _ = Nothing
+ eq_type _ _ = Nothing
instance -- Eq
- Type_Eq root =>
+ Eq_Type root =>
Eq (Type_Tuple2 root h) where
- x == y = isJust $ type_eq x y
+ x == y = isJust $ eq_type x y
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Tuple2 root) where
type instance Root_of_Type (Type_Unit root) = root
type instance Error_of_Type ast (Type_Unit root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq (Type_Unit root) where
- type_eq Type_Unit Type_Unit = Just Refl
+instance -- Eq_Type
+ Eq_Type (Type_Unit root) where
+ eq_type Type_Unit Type_Unit = Just Refl
instance -- Eq
Eq (Type_Unit root h) where
- x == y = isJust $ x `type_eq` y
+ x == y = isJust $ x `eq_type` y
instance -- String_from_Type
String_from_Type (Type_Unit root) where
string_from_type Type_Unit = "Unit"
instance -- Show
Show (Type_Unit root h) where
show = string_from_type
-instance Type_Constraint Eq (Type_Unit root) where
- type_constraint _c Type_Unit = Just Dict
-instance Type_Constraint Ord (Type_Unit root) where
- type_constraint _c Type_Unit = Just Dict
+instance Constraint_Type Eq (Type_Unit root) where
+ constraint_type _c Type_Unit = Just Dict
+instance Constraint_Type Ord (Type_Unit root) where
+ constraint_type _c Type_Unit = Just Dict
-- | Convenient alias to include a 'Type_Unit' within a type.
type_unit :: Type_Root_Lift Type_Unit root => root ()
type instance Root_of_Type (Type_Var root) = root
type instance Error_of_Type ast (Type_Var root) = No_Error_Type
-instance -- Type_Eq
- Type_Eq (Type_Var root) where
- type_eq (Type_Var x) (Type_Var y) = x `peano_eq` y
+instance -- Eq_Type
+ Eq_Type (Type_Var root) where
+ eq_type (Type_Var x) (Type_Var y) = x `peano_eq` y
instance -- Eq
Eq (Type_Var root h) where
- x == y = isJust $ x `type_eq` y
+ x == y = isJust $ x `eq_type` y
instance -- String_from_Type
String_from_Type (Type_Var root) where
string_from_type (Type_Var p) =
instance -- Show
Show (Type_Var root h) where
show = string_from_type
-instance Type_Constraint Eq (Type_Var root)
-instance Type_Constraint Ord (Type_Var root)
+instance Constraint_Type Eq (Type_Var root)
+instance Constraint_Type Ord (Type_Var root)
-- | Convenient alias to include a 'Type_Var' within a type.
type_var :: Type_Root_Lift Type_Var root => SPeano p -> root p
and then interpret them at will.
.
Your comments, problem reports, or questions are very welcome! :-)
+ .
+ NOTE: alternative libraries to do more or less the same things
+ include: <https://hackage.haskell.org/package/syntactic syntactic>.
extra-source-files:
extra-tmp-files:
-- homepage: http://pad.autogeree.net/informatique/symantic/
sourcephile / git / haskell / symantic.git / commitdiff