]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/If.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / If.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE UndecidableInstances #-}
11 module Language.LOL.Symantic.Expr.If where
12
13 import Data.Proxy (Proxy(..))
14 import Data.Type.Equality ((:~:)(Refl))
15 import Language.LOL.Symantic.AST
16 import Language.LOL.Symantic.Expr.Bool
17 import Language.LOL.Symantic.Expr.Common
18 import Language.LOL.Symantic.Expr.Lambda
19 import Language.LOL.Symantic.Repr.Dup
20 import Language.LOL.Symantic.Trans.Common
21 import Language.LOL.Symantic.Type
22
23 -- * Class 'Sym_If'
24
25 class Sym_If repr where
26 if_ :: repr Bool -> repr a -> repr a -> repr a
27 when_ :: repr Bool -> repr () -> repr ()
28
29 default if_ :: Trans t repr => t repr Bool -> t repr a -> t repr a -> t repr a
30 default when_ :: Trans t repr => t repr Bool -> t repr () -> t repr ()
31 if_ = trans_map3 if_
32 when_ = trans_map2 when_
33
34 instance -- Sym_If Dup
35 ( Sym_If r1
36 , Sym_If r2
37 ) => Sym_If (Dup r1 r2) where
38 if_ (c1 `Dup` c2) (ok1 `Dup` ok2) (ko1 `Dup` ko2) =
39 if_ c1 ok1 ko1 `Dup`
40 if_ c2 ok2 ko2
41 when_ (c1 `Dup` c2) (ok1 `Dup` ok2) =
42 when_ c1 ok1 `Dup`
43 when_ c2 ok2
44
45 -- * Type 'Expr_If'
46 -- | Expression.
47 data Expr_If (root:: *)
48 type instance Root_of_Expr (Expr_If root) = root
49 type instance Type_of_Expr (Expr_If root) = No_Type
50 type instance Sym_of_Expr (Expr_If root) repr = (Sym_If repr)
51 type instance Error_of_Expr ast (Expr_If root) = No_Error_Expr
52
53 instance -- Expr_from AST Expr_If
54 ( Type_from AST (Type_Root_of_Expr root)
55 , Expr_from AST root
56 , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
57 , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
58 ( Type_Root_of_Expr root)
59 AST)
60 (Error_of_Expr AST root)
61 , Root_of_Expr root ~ root
62 , Implicit_HBool (Is_Last_Expr (Expr_If root) root)
63 ) => Expr_from AST (Expr_If root) where
64 expr_from px_ex ctx ast k =
65 case ast of
66 AST "if" asts ->
67 case asts of
68 [ast_cond, ast_ok, ast_ko] ->
69 expr_from (Proxy::Proxy root) ctx ast_cond $
70 \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
71 expr_from (Proxy::Proxy root) ctx ast_ok $
72 \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
73 expr_from (Proxy::Proxy root) ctx ast_ko $
74 \(ty_ko::Type_Root_of_Expr root h_ko) (Forall_Repr_with_Context ko) ->
75 when_type_eq px_ex ast
76 type_bool ty_cond $ \Refl ->
77 when_type_eq px_ex ast
78 ty_ok ty_ko $ \Refl ->
79 k ty_ok $ Forall_Repr_with_Context $
80 \c -> if_ (cond c) (ok c) (ko c)
81 _ -> Left $ error_expr px_ex $
82 Error_Expr_Wrong_number_of_arguments ast 3
83 _ -> Left $ error_expr_unsupported px_ex ast
84
85 -- ** Type 'Expr_Lambda_Bool_If'
86 -- | Convenient alias.
87 type Expr_Lambda_If_Bool lam
88 = Expr_Root (Expr_Alt (Expr_Lambda lam)
89 (Expr_Alt Expr_If
90 Expr_Bool))
91
92 -- | Convenient alias around 'expr_from'.
93 expr_lambda_if_bool_from
94 :: forall lam ast root.
95 ( Expr_from ast (Expr_Lambda_If_Bool lam)
96 , root ~ Expr_Lambda_If_Bool lam
97 ) => Proxy lam
98 -> ast
99 -> Either (Error_of_Expr ast root)
100 (Exists_Type_and_Repr (Type_Root_of_Expr root)
101 (Forall_Repr root))
102 expr_lambda_if_bool_from _px_lam ast =
103 expr_from
104 (Proxy::Proxy root)
105 Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
106 Right $ Exists_Type_and_Repr ty $
107 Forall_Repr $ repr Context_Empty