Update doc.

[haskell/symantic.git] / Language / Symantic / Typing / Constant.hs

diff --git a/Language/Symantic/Typing/Constant.hs b/Language/Symantic/Typing/Constant.hs
index c250aefd7fb85ef83bc5a6deddb555343a9c917c..2cd31e8334c0c50343675cec482168a5e15451c5 100644 (file)
--- a/Language/Symantic/Typing/Constant.hs
+++ b/Language/Symantic/Typing/Constant.hs
@@ -11,11 +11,10 @@ import Data.NonNull (NonNull)
 import Data.Proxy
 import Data.Text (Text)
 import Data.Type.Equality
-import GHC.Exts (Constraint)
 import qualified System.IO as IO
 
-import Language.Symantic.Lib.Data.Type.List
-import Language.Symantic.Lib.Data.Type.Peano
+import Language.Symantic.Helper.Data.Type.List
+import Language.Symantic.Helper.Data.Type.Peano
 import Language.Symantic.Typing.Kind
 
 -- * Type 'Const'
@@ -48,7 +47,7 @@ type Inj_Const cs c = Inj_ConstP (Index cs (Proxy c)) cs c
 -- | Inject a given /type constant/ @c@ into a list of them,
 -- by returning a proof that 'Proxy'@ c@ is in @cs@.
 inj_const :: forall cs c. Inj_Const cs c => Const cs c
-inj_const = inj_constP (Proxy::Proxy (Index cs (Proxy c)))
+inj_const = inj_constP (Proxy @(Index cs (Proxy c)))
 
 -- ** Class 'Inj_ConstP'
 class Inj_ConstP p cs c where
@@ -65,7 +64,7 @@ instance
  ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
        inj_constP _ = ConstZ (kindP (Proxy :: Proxy (Ty_of_Type k)))
 instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
-       inj_constP _p = ConstS (inj_constP (Proxy::Proxy p))
+       inj_constP _p = ConstS (inj_constP (Proxy @p))
 
 -- * Class 'Proj_Const'
 -- | Convenient type synonym wrapping 'Proj_ConstP'
@@ -76,10 +75,10 @@ type Proj_Const cs c = Proj_ConstP (Index cs (Proxy c)) cs c
 -- returning a proof that the 'Const' indexes @c@ iif. it's the case.
 proj_const :: forall cs k (c::k) (u::k).
  Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
-proj_const = proj_constP (Proxy::Proxy (Index cs (Proxy c)))
+proj_const = proj_constP (Proxy @(Index cs (Proxy c)))
 
 (=?) :: forall cs c u. Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
-(=?) = proj_constP (Proxy::Proxy (Index cs (Proxy c)))
+(=?) = proj_constP (Proxy @(Index cs (Proxy c)))
 
 -- ** Type 'Proj_ConstP'
 class Proj_ConstP p cs c where
@@ -89,41 +88,17 @@ instance Proj_ConstP Zero (Proxy c ': cs) c where
        proj_constP _p ConstS{} _c = Nothing
 instance Proj_ConstP p cs c => Proj_ConstP (Succ p) (not_c ': cs) c where
        proj_constP _p ConstZ{} _c  = Nothing
-       proj_constP _p (ConstS u) c = proj_constP (Proxy::Proxy p) u c
+       proj_constP _p (ConstS u) c = proj_constP (Proxy @p) u c
 
 -- ** Type 'Proj_Consts'
 type Proj_Consts cs cs_to_proj
  = Concat_Constraints (Proj_ConstsR cs cs_to_proj)
 
 -- *** Type family 'Proj_ConstsR'
-type family Proj_ConstsR cs cs_to_proj :: [Constraint] where
+type family Proj_ConstsR cs cs_to_proj where
  Proj_ConstsR cs '[] = '[]
  Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs
 
--- * Class 'Const_from'
--- | Try to build a 'Const' from raw data.
-class Const_from raw cs where
-       const_from
-        :: raw -> (forall k c. Const cs (c::k) -> Maybe ret)
-        -> Maybe ret
-
-instance Const_from raw '[] where
-       const_from _c _k = Nothing
-
--- TODO: move each of these to a dedicated module.
-instance Const_from Text cs => Const_from Text (Proxy Bounded ': cs) where
-       const_from "Bounded" k = k (ConstZ kind)
-       const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy Enum ': cs) where
-       const_from "Enum" k = k (ConstZ kind)
-       const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy Fractional ': cs) where
-       const_from "Fractional" k = k (ConstZ kind)
-       const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy Real ': cs) where
-       const_from "Real" k = k (ConstZ kind)
-       const_from s k = const_from s $ k . ConstS
-
 -- * Class 'Show_Const'
 class Show_Const cs where
        show_const :: Const cs c -> String