]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Unit.hs
Reorganize symantic-document modules.
[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 Language.Symantic
7 import Language.Symantic.Grammar
8
9 -- * Class 'Sym_Unit'
10 type instance Sym () = Sym_Unit
11 class Sym_Unit term where
12 unit :: term ()
13 default unit :: Sym_Unit (UnT term) => Trans term => term ()
14 unit = trans unit
15
16 -- Interpreting
17 instance Sym_Unit Eval where
18 unit = Eval ()
19 instance Sym_Unit View where
20 unit = View $ \_p _v -> "()"
21 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
22 unit = unit `Dup` unit
23
24 -- Transforming
25 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
26
27 -- Typing
28 instance NameTyOf () where
29 nameTyOf _c = [] `Mod` ""
30 instance ClassInstancesFor () where
31 proveConstraintFor _ (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_Source src g
47 , Gram_Rule g
48 , Gram_Comment g
49 , SymInj ss ()
50 ) => Gram_Term_AtomsFor src ss g () where
51 g_term_atomsFor =
52 [ rule "teUnit" $
53 source $
54 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
55 <$ symbol "("
56 <* symbol ")"
57 ]
58 instance ModuleFor src ss ()
59
60 -- ** 'Type's
61 tyUnit :: Source src => LenInj vs => Type src vs ()
62 tyUnit = tyConst @(K ()) @()
63
64 -- ** 'Term's
65 teUnit :: TermDef () '[] (() #> ())
66 teUnit = Term noConstraint tyUnit $ teSym @() $ unit