]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Unit.hs
Massive rewrite to better support rank-1 polymorphic types.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Unit.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for '()'.
4 module Language.Symantic.Lib.Unit where
5
6 import Prelude hiding ((&&), not, (||))
7
8 import Language.Symantic
9 import Language.Symantic.Grammar
10
11 -- * Class 'Sym_Unit'
12 type instance Sym (Proxy ()) = Sym_Unit
13 class Sym_Unit term where
14 unit :: term ()
15 default unit :: Sym_Unit (UnT term) => Trans term => term ()
16 unit = trans unit
17
18 -- Interpreting
19 instance Sym_Unit Eval where
20 unit = Eval ()
21 instance Sym_Unit View where
22 unit = View $ \_p _v -> "()"
23 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
24 unit = unit `Dup` unit
25
26 -- Transforming
27 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
28
29 -- Typing
30 instance ClassInstancesFor () where
31 proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
32 | Just HRefl <- proj_ConstKiTy @_ @() z
33 = case () of
34 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
35 | Just Refl <- proj_Const @Enum q -> Just Dict
36 | Just Refl <- proj_Const @Eq q -> Just Dict
37 | Just Refl <- proj_Const @Monoid q -> Just Dict
38 | Just Refl <- proj_Const @Ord q -> Just Dict
39 | Just Refl <- proj_Const @Show q -> Just Dict
40 _ -> Nothing
41 proveConstraintFor _c _q = Nothing
42 instance TypeInstancesFor ()
43
44 -- Compiling
45 instance
46 ( Gram_Rule g
47 , Gram_Comment g
48 , Gram_Meta src g
49 , Inj_Sym ss ()
50 , Source src
51 ) => Gram_Term_AtomsFor src ss g () where
52 g_term_atomsFor _t =
53 [ rule "teUnit" $
54 withMeta $
55 (\src -> BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teUnit)
56 <$ symbol "("
57 <* symbol ")"
58 ]
59 instance Module src ss ()
60
61 -- ** 'Type's
62 tyUnit :: Source src => Inj_Len vs => Type src vs ()
63 tyUnit = tyConst @(K ()) @()
64
65 -- ** 'Term's
66 teUnit ::
67 Source src => Inj_Sym ss () =>
68 Term src ss ts '[] ()
69 teUnit = Term noConstraint tyUnit $ teSym @() $ unit