{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
-- | Expression for 'Maybe'.
module Language.LOL.Symantic.Expr.Maybe where
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)
-import Language.LOL.Symantic.AST
import Language.LOL.Symantic.Type
import Language.LOL.Symantic.Repr.Dup
import Language.LOL.Symantic.Trans.Common
type instance Root_of_Expr (Expr_Maybe lam root) = root
type instance Type_of_Expr (Expr_Maybe lam root) = Type_Maybe
type instance Sym_of_Expr (Expr_Maybe lam root) repr = (Sym_Maybe lam repr, Sym_Maybe_Cons repr)
-type instance Error_of_Expr ast (Expr_Maybe lam root) = ()
+type instance Error_of_Expr ast (Expr_Maybe lam root) = No_Error_Expr
-instance -- Expr_from AST Expr_Maybe
- ( Type_from AST (Type_Root_of_Expr root)
- , Expr_from AST root
-
+maybe_from
+ :: forall root lam ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
+ , Type_Eq (Type_Root_of_Expr root)
+ , Expr_from ast root
, Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
, Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
- , Error_Type_Lift (Error_Type_Fun AST)
- (Error_of_Type AST (Type_Root_of_Expr root))
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
- ( Type_Root_of_Expr root)
- AST)
- (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
- ( Type_Root_of_Expr root)
- AST)
- (Error_of_Expr AST root)
-
+ , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
, Type_Unlift (Type_Fun lam) (Type_of_Expr root)
, Type_Unlift Type_Maybe (Type_of_Expr root)
-
, Root_of_Expr root ~ root
-
- , Implicit_HBool (Is_Last_Expr (Expr_Maybe lam root) root)
- ) => Expr_from AST (Expr_Maybe lam root) where
- expr_from px_ex ctx ast k =
- case ast of
- AST "maybe" asts ->
- case asts of
- [ast_n, ast_j, ast_m] ->
- expr_from (Proxy::Proxy root) ctx ast_n $
- \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
- expr_from (Proxy::Proxy root) ctx ast_j $
- \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
- expr_from (Proxy::Proxy root) ctx ast_m $
- \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
- case type_unlift $ unType_Root ty_j of
- Just (ty_j_a `Type_Fun` ty_j_b
- :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
- case type_unlift $ unType_Root ty_m of
- Just (Type_Maybe ty_m_a
- :: Type_Maybe (Type_Root_of_Expr root) h_m) ->
- when_type_eq px_ex ast
- ty_n ty_j_b $ \Refl ->
- when_type_eq px_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 $ error_expr px_ex $
- Error_Expr_Wrong_number_of_arguments 3 ast
- AST "nothing" asts ->
- case asts of
- [ast_ty_a] ->
- case type_from
- (Proxy::Proxy (Type_Root_of_Expr root))
- ast_ty_a (Right . Exists_Type) of
- Left err -> Left $ error_expr px_ex $ Error_Expr_Type err ast
- Right (Exists_Type (ty_a::Type_Root_of_Expr root h_a)) ->
- k (type_maybe ty_a) $ Forall_Repr_with_Context $
- const nothing
- _ -> Left $ error_expr px_ex $
- Error_Expr_Wrong_number_of_arguments 1 ast
- AST "just" asts ->
- case asts of
- [ast_a] ->
- expr_from (Proxy::Proxy root) ctx ast_a $
- \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
- k (type_maybe ty_a) $ Forall_Repr_with_Context $
- \c -> just (a c)
- _ -> Left $ error_expr px_ex $
- Error_Expr_Wrong_number_of_arguments 1 ast
- _ -> Left $
- case hbool :: HBool (Is_Last_Expr (Expr_Maybe lam root) root) of
- HTrue -> error_expr px_ex $ Error_Expr_Unsupported ast
- HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
+ ) => ast -> ast -> ast
+ -> Expr_From ast (Expr_Maybe lam root) hs ret
+maybe_from ast_n ast_j ast_m ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_n ctx $
+ \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
+ expr_from (Proxy::Proxy root) ast_j ctx $
+ \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
+ case type_unlift $ unType_Root ty_j of
+ Nothing -> Left $
+ error_expr ex $
+ Error_Expr_Type_mismatch ast
+ (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
+ :: Type_Root_of_Expr (Expr_Maybe lam root) (lam Zero -> lam (Succ Zero))))
+ (Exists_Type ty_m)
+ Just (ty_j_a `Type_Fun` ty_j_b
+ :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
+ case type_unlift $ unType_Root ty_m of
+ Nothing -> Left $
+ error_expr ex $
+ Error_Expr_Type_mismatch ast
+ (Exists_Type (type_maybe $ type_var SZero
+ :: Type_Root_of_Expr (Expr_Maybe lam root) (Maybe Zero)))
+ (Exists_Type ty_m)
+ Just (Type_Maybe ty_m_a
+ :: Type_Maybe (Type_Root_of_Expr root) h_m) ->
+ when_type_eq ex ast
+ ty_n ty_j_b $ \Refl ->
+ when_type_eq ex ast
+ ty_m_a ty_j_a $ \Refl ->
+ k ty_n $ Forall_Repr_with_Context $
+ \c -> maybe (n c) (j c) (m c)
+nothing_from
+ :: forall root lam ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
+ , Type_from ast (Type_Root_of_Expr root)
+ , Type_Root_Lift Type_Maybe (Type_Root_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
+ ) => ast
+ -> Expr_From ast (Expr_Maybe lam root) hs ret
+nothing_from ast_ty_a ex ast _ctx k =
+ case type_from
+ (Proxy::Proxy (Type_Root_of_Expr root))
+ ast_ty_a (Right . Exists_Type) of
+ Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
+ Right (Exists_Type (ty_a::Type_Root_of_Expr root h_a)) ->
+ k (type_maybe ty_a) $ Forall_Repr_with_Context $
+ const nothing
+
+just_from
+ :: forall root lam ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
+ , Expr_from ast root
+ , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
+ , Root_of_Expr root ~ root
+ ) => ast
+ -> Expr_From ast (Expr_Maybe lam root) hs ret
+just_from ast_a _ex _ast ctx k =
+ expr_from (Proxy::Proxy root) ast_a ctx $
+ \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
+ k (type_maybe ty_a) $ Forall_Repr_with_Context $
+ \c -> just (a c)
--- ** Type 'Expr_Lambda_Bool_Maybe'
+-- ** Type 'Expr_Lambda_Maybe_Bool'
-- | Convenient alias.
-type Expr_Lambda_Bool_Maybe lam
+type Expr_Lambda_Maybe_Bool lam
= Expr_Root (Expr_Alt (Expr_Lambda lam)
- (Expr_Alt Expr_Bool
- (Expr_Maybe lam)))
+ (Expr_Alt (Expr_Maybe lam)
+ Expr_Bool))
-- | Convenient alias around 'expr_from'.
-expr_lambda_bool_maybe_from
+expr_lambda_maybe_bool_from
:: forall lam ast root.
- ( Expr_from ast (Expr_Lambda_Bool_Maybe lam)
- , root ~ Expr_Lambda_Bool_Maybe lam
+ ( Expr_from ast (Expr_Lambda_Maybe_Bool lam)
+ , root ~ Expr_Lambda_Maybe_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_bool_maybe_from _px_lam ast =
- expr_from
- (Proxy::Proxy root)
- Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
+expr_lambda_maybe_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
sourcephile / git / haskell / symantic.git / blobdiff