1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# OPTIONS_GHC -fno-warn-orphans #-}
13 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
14 -- | Symantic for @if@.
15 module Language.Symantic.Compiling.If where
17 import Data.Monoid ((<>))
19 import Data.String (IsString)
20 import Data.Text (Text)
21 import Data.Type.Equality ((:~:)(Refl))
23 import Language.Symantic.Typing
24 import Language.Symantic.Compiling.Term
25 import Language.Symantic.Compiling.Bool (tyBool)
26 import Language.Symantic.Interpreting
27 import Language.Symantic.Transforming.Trans
30 class Sym_If term where
31 if_ :: term Bool -> term a -> term a -> term a
32 default if_ :: Trans t term => t term Bool -> t term a -> t term a -> t term a
37 type instance Sym_of_Iface (Proxy If) = Sym_If
38 type instance Consts_of_Iface (Proxy If) = Consts_imported_by If
39 type instance Consts_imported_by If =
43 instance Sym_If HostI where
44 if_ (HostI b) ok ko = if b then ok else ko
45 instance Sym_If TextI where
46 if_ (TextI cond) (TextI ok) (TextI ko) =
48 let p' = Precedence 2 in
51 " then " <> ok p' v <>
53 instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
54 if_ = dupI3 sym_If if_
56 instance Const_from Text cs => Const_from Text (Proxy If ': cs) where
57 const_from s k = const_from s $ k . ConstS
60 Proj_ConC cs (Proxy If)
61 instance -- Term_fromI
63 , Lexem ast ~ LamVarName
64 , Inj_Const (Consts_of_Ifaces is) Bool
66 ) => Term_fromI is (Proxy If) ast where
67 term_fromI ast ctx k =
70 _ -> Left $ Error_Term_unsupported
73 -- if :: Bool -> a -> a -> a
74 from_ast3 ast $ \ast_cond ast_ok ast_ko as ->
75 term_from ast_cond ctx $ \ty_cond (TermLC cond) ->
76 term_from ast_ok ctx $ \ty_ok (TermLC ok) ->
77 term_from ast_ko ctx $ \ty_ko (TermLC ko) ->
78 check_type (At Nothing tyBool) (At (Just ast_cond) ty_cond) $ \Refl ->
79 check_type (At (Just ast_ok) ty_ok) (At (Just ast_ko) ty_ko) $ \Refl ->
81 \c -> if_ (cond c) (ok c) (ko c)
83 sym_If :: Proxy Sym_If
86 syIf :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
87 syIf cond ok ko = Syntax "if" [cond, ok, ko]