From 4cd74b2c501118e9402b74bd4dfe62518ffcfe4f Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm+lol@autogeree.net>
Date: Sun, 2 Oct 2016 15:46:42 +0200
Subject: [PATCH] init
---
Language/LOL/Symantic/Expr/Bool.hs | 24 ++++++++++--------------
Language/LOL/Symantic/Expr/Bool/Test.hs | 10 +---------
Language/LOL/Symantic/Expr/Common.hs | 9 +++++++++
Language/LOL/Symantic/Expr/Int.hs | 24 ++++++++++--------------
Language/LOL/Symantic/Expr/Int/Test.hs | 10 +---------
Language/LOL/Symantic/Expr/Lambda.hs | 22 +++++++++-------------
6 files changed, 40 insertions(+), 59 deletions(-)
diff --git a/Language/LOL/Symantic/Expr/Bool.hs b/Language/LOL/Symantic/Expr/Bool.hs
index 5664833..b2c566d 100644
--- a/Language/LOL/Symantic/Expr/Bool.hs
+++ b/Language/LOL/Symantic/Expr/Bool.hs
@@ -77,17 +77,17 @@ instance -- Expr_from AST Expr_Bool
, Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
) => Expr_from AST (Expr_Bool root) where
- expr_from _px_ex ctx ast k =
+ expr_from px_ex ctx ast k =
case ast of
AST "bool" asts ->
case asts of
[AST ast_bool []] ->
case read_safe ast_bool of
- Left err -> Left $ error_expr $ Error_Expr_Read err ast
+ Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
Right (i::Bool) ->
k type_bool $ Forall_Repr_with_Context $
const $ bool i
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
AST "not" asts -> unary_from asts not
AST "and" asts -> binary_from asts and
@@ -95,8 +95,8 @@ instance -- Expr_from AST Expr_Bool
AST "xor" asts -> binary_from asts xor
_ -> Left $
case hbool :: HBool (Is_Last_Expr (Expr_Bool root) root) of
- HTrue -> error_expr $ Error_Expr_Unsupported ast
- HFalse -> error_expr $ Error_Expr_Unsupported_here ast
+ HTrue -> error_expr px_ex $ Error_Expr_Unsupported ast
+ HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
where
unary_from asts
(op::forall repr. Sym_Bool repr
@@ -108,11 +108,11 @@ instance -- Expr_from AST Expr_Bool
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 $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_bool)
(Exists_Type ty_x) ast
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 1 ast
binary_from asts
(op::forall repr. Sym_Bool repr
@@ -129,20 +129,16 @@ instance -- Expr_from AST Expr_Bool
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 $ error_expr $
+ Nothing -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_bool)
(Exists_Type ty_y) ast
- Nothing -> Left $ error_expr $
+ Nothing -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_bool)
(Exists_Type ty_x) ast
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 2 ast
- error_expr
- :: Error_Expr (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
- -> Error_of_Expr AST root
- error_expr = error_expr_lift
-- ** Type 'Expr_Lambda_Bool'
-- | Convenient alias.
diff --git a/Language/LOL/Symantic/Expr/Bool/Test.hs b/Language/LOL/Symantic/Expr/Bool/Test.hs
index 41fd3fb..8776808 100644
--- a/Language/LOL/Symantic/Expr/Bool/Test.hs
+++ b/Language/LOL/Symantic/Expr/Bool/Test.hs
@@ -66,7 +66,7 @@ e8 = x `xor` (y `xor` bool True)
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case ty `type_eq` ty_expected of
Nothing -> return $ Left $
- error_expr $ Error_Expr_Type
+ error_expr (Proxy::Proxy root) $ Error_Expr_Type
(error_type_lift $ Error_Type_Unsupported_here raw) raw
Just Refl -> do
h <- host_from_expr r
@@ -77,14 +77,6 @@ e8 = x `xor` (y `xor` bool True)
, string_from_expr r
-- , (string_from_expr :: Repr_String IO h -> String) r
)
- where
- error_expr
- :: (root ~ Expr_Lambda_Bool IO)
- => Error_Expr (Error_of_Type raw (Type_Root_of_Expr root))
- (Type_Root_of_Expr root)
- raw
- -> Error_of_Expr raw root
- error_expr = error_expr_lift
tests :: TestTree
tests = testGroup "Bool" $
diff --git a/Language/LOL/Symantic/Expr/Common.hs b/Language/LOL/Symantic/Expr/Common.hs
index edeebcd..3072ccf 100644
--- a/Language/LOL/Symantic/Expr/Common.hs
+++ b/Language/LOL/Symantic/Expr/Common.hs
@@ -366,3 +366,12 @@ data Error_Expr err_ty ty ast
| Error_Expr_Unsupported_here ast
-- ^ Given syntax not supported by the current expression parser component.
deriving (Eq, Show)
+
+error_expr
+ :: Error_Expr_Lift
+ (Error_Expr (Error_of_Type ast (Type_Root_of_Expr ex)) (Type_Root_of_Expr ex) ast)
+ (Error_of_Expr ast (Root_of_Expr ex))
+ => Proxy ex
+ -> Error_Expr (Error_of_Type ast (Type_Root_of_Expr ex)) (Type_Root_of_Expr ex) ast
+ -> Error_of_Expr ast (Root_of_Expr ex)
+error_expr _ = error_expr_lift
diff --git a/Language/LOL/Symantic/Expr/Int.hs b/Language/LOL/Symantic/Expr/Int.hs
index 2bc239b..470bbf9 100644
--- a/Language/LOL/Symantic/Expr/Int.hs
+++ b/Language/LOL/Symantic/Expr/Int.hs
@@ -70,24 +70,24 @@ instance -- Expr_from AST Expr_Int
, Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
) => Expr_from AST (Expr_Int root) where
- expr_from _px_ex ctx ast k =
+ expr_from px_ex ctx ast k =
case ast of
AST "int" asts ->
case asts of
[AST ast_int []] ->
case read_safe ast_int of
- Left err -> Left $ error_expr $ Error_Expr_Read err ast
+ Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
Right (i::Int) ->
k type_int $ Forall_Repr_with_Context $
const $ int i
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
AST "neg" asts -> unary_from asts neg
AST "add" asts -> binary_from asts add
_ -> Left $
case hbool :: HBool (Is_Last_Expr (Expr_Int root) root) of
- HTrue -> error_expr $ Error_Expr_Unsupported ast
- HFalse -> error_expr $ Error_Expr_Unsupported_here ast
+ HTrue -> error_expr px_ex $ Error_Expr_Unsupported ast
+ HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
where
unary_from asts
(op::forall repr. Sym_Int repr
@@ -99,11 +99,11 @@ instance -- Expr_from AST Expr_Int
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 $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_int)
(Exists_Type ty_x) ast
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 1 ast
binary_from asts
(op::forall repr. Sym_Int repr
@@ -120,20 +120,16 @@ instance -- Expr_from AST Expr_Int
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 $ error_expr $
+ Nothing -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_int)
(Exists_Type ty_y) ast
- Nothing -> Left $ error_expr $
+ Nothing -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type type_int)
(Exists_Type ty_x) ast
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 2 ast
- error_expr
- :: Error_Expr (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
- -> Error_of_Expr AST root
- error_expr = error_expr_lift
-- ** Type 'Expr_Lambda_Int'
-- | Convenient alias.
diff --git a/Language/LOL/Symantic/Expr/Int/Test.hs b/Language/LOL/Symantic/Expr/Int/Test.hs
index 312c4b2..e4aa1b8 100644
--- a/Language/LOL/Symantic/Expr/Int/Test.hs
+++ b/Language/LOL/Symantic/Expr/Int/Test.hs
@@ -59,7 +59,7 @@ e8 = x `add` (y `add` int 1)
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case ty `type_eq` ty_expected of
Nothing -> return $ Left $
- error_expr $ Error_Expr_Type
+ error_expr (Proxy::Proxy root) $ Error_Expr_Type
(error_type_lift $ Error_Type_Unsupported raw) raw
Just Refl -> do
h <- host_from_expr r
@@ -70,14 +70,6 @@ e8 = x `add` (y `add` int 1)
, string_from_expr r
-- , (string_from_expr :: Repr_String IO h -> String) r
)
- where
- error_expr
- :: (root ~ Expr_Lambda_Int IO)
- => Error_Expr (Error_of_Type raw (Type_Root_of_Expr root))
- (Type_Root_of_Expr root)
- raw
- -> Error_of_Expr raw root
- error_expr = error_expr_lift
tests :: TestTree
tests = testGroup "Int" $
diff --git a/Language/LOL/Symantic/Expr/Lambda.hs b/Language/LOL/Symantic/Expr/Lambda.hs
index be985ed..ed1a28a 100644
--- a/Language/LOL/Symantic/Expr/Lambda.hs
+++ b/Language/LOL/Symantic/Expr/Lambda.hs
@@ -141,7 +141,7 @@ instance -- Expr_from AST Expr_Lambda
, Implicit_HBool (Is_Last_Expr (Expr_Lambda lam root) root)
-- NOTE: require UndecidableInstances.
) => Expr_from AST (Expr_Lambda lam root) where
- expr_from _px_ex ctx ast k =
+ expr_from px_ex ctx ast k =
case ast of
AST "var" asts ->
case asts of
@@ -166,7 +166,7 @@ instance -- Expr_from AST Expr_Lambda
go ctx' $ \ty (Forall_Repr_with_Context repr) ->
k' ty $ Forall_Repr_with_Context $
\(_ `Context_Alt_Next` c') -> repr c'
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 1 ast
AST "app" asts ->
case asts of
@@ -183,13 +183,13 @@ instance -- Expr_from AST Expr_Lambda
Just Refl ->
k ty_res $ Forall_Repr_with_Context $
\c -> lam c `app` arg_actual c
- Nothing -> Left $ error_expr $
+ Nothing -> Left $ error_expr px_ex $
Error_Expr_Fun_Argument_mismatch
(Exists_Type ty_arg_expected)
(Exists_Type ty_arg_actual) ast
Nothing -> Left $ error_expr_lift $
Error_Expr_Lambda_Not_a_lambda ast
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Type (error_type_lift $
Error_Type_Fun_Wrong_number_of_arguments 2 ast) ast
AST "inline" asts -> lambda_from asts inline
@@ -200,8 +200,8 @@ instance -- Expr_from AST Expr_Lambda
AST "let_lazy" asts -> let_from asts let_lazy
_ -> Left $
case hbool :: HBool (Is_Last_Expr (Expr_Lambda lam root) root) of
- HTrue -> error_expr $ Error_Expr_Unsupported ast
- HFalse -> error_expr $ Error_Expr_Unsupported_here ast
+ HTrue -> error_expr px_ex $ Error_Expr_Unsupported ast
+ HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
where
lambda_from asts
(lam::forall repr arg res. Sym_Lambda lam repr
@@ -212,7 +212,7 @@ instance -- Expr_from AST Expr_Lambda
(Proxy::Proxy (Type_Root_of_Expr root))
ast_ty_arg
(Right . Exists_Type) of
- Left err -> Left $ error_expr $ Error_Expr_Type err ast
+ Left err -> Left $ error_expr px_ex $ 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_Alt_Next` ctx) ast_body $
@@ -223,7 +223,7 @@ instance -- Expr_from AST Expr_Lambda
Forall_Repr_with_Context $
\c -> lam $
\arg -> res (arg `Context_Alt_Next` c)
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
let_from asts
(let_::forall repr var res. Sym_Lambda lam repr
@@ -238,12 +238,8 @@ instance -- Expr_from AST Expr_Lambda
k ty_res $ Forall_Repr_with_Context $
\c -> let_ (var c) $
\arg -> res (arg `Context_Alt_Next` c)
- _ -> Left $ error_expr $
+ _ -> Left $ error_expr px_ex $
Error_Expr_Fun_Wrong_number_of_arguments 3 ast
- error_expr
- :: Error_Expr (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
- -> Error_of_Expr AST root
- error_expr = error_expr_lift
-- * Type 'Error_Expr_Lambda'
data Error_Expr_Lambda ast
--
2.47.2