Add common instances to Interpreting.Dup.
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Read.hs
index 3199ef41a52ab95b76c3b7787d0c67f9b0de013e..8d857fae3016cc3cc0c190148d3139f04916ede8 100644 (file)
@@ -2,13 +2,7 @@
 {-# LANGUAGE PolyKinds #-}
 module Language.Symantic.Typing.Read where
 
-import Data.Map.Strict (Map)
-import Data.Typeable
-import qualified Data.Map.Strict as Map
-import qualified Data.Text as Text
-
 import Language.Symantic.Grammar
-import Language.Symantic.Typing.List
 import Language.Symantic.Typing.Kind
 import Language.Symantic.Typing.Type
 import Language.Symantic.Typing.Show ()
@@ -17,50 +11,37 @@ import Language.Symantic.Typing.Variable
 
 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
 readType ::
- Inj_Source (KindK src) src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (AST_Type src) src =>
- Name2Type src ->
+ SourceInj (KindK src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (AST_Type src) src =>
  AST_Type src ->
  Either (Error_Type src) (TypeVT src)
-readType cs ast | EVars vs <- readVars (EVars VarsZ) ast = do
-       TypeT ty <- readTyVars cs vs ast
+readType ast | EVars vs <- readVars (EVars VarsZ) ast = do
+       TypeT ty <- readTyVars vs ast
        Right $ TypeVT ty
 
 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
 readTyVars ::
  forall vs src.
- Inj_Source (KindK src) src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (AST_Type src) src =>
- Name2Type src ->
+ SourceInj (KindK src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (AST_Type src) src =>
  Vars src vs ->
  AST_Type src ->
  Either (Error_Type src) (TypeT src vs)
-readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
-       readTyName cs (inj_Source ast) (lenVars vs) name
-readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
+readTyVars vs (BinTree0 (Token_Type_Const (TypeTLen t))) =
+       Right $ t (lenVars vs)
+       -- readTyName is ms (sourceInj ast) (lenVars vs) name
+readTyVars vs (BinTree0 (Token_Type_Var (At src name))) =
        case lookupVars name vs of
-        Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
+        Just (EVar v) -> Right $ TypeT $ TyVar src name v
         Nothing -> error "[BUG] readTyVars: lookupVars failed"
-readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do
-       TypeT ty_x <- readTyVars cs vs ast_x
-       TypeT ty_y <- readTyVars cs vs ast_y
+readTyVars vs ast@(ast_x `BinTree2` ast_y) = do
+       TypeT ty_x <- readTyVars vs ast_x
+       TypeT ty_y <- readTyVars vs ast_y
        when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
                when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
-                       Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y
-
--- | Lookup a 'TyConst' or 'Type' synonym
--- associated with given 'NameTy' in given 'Name2Type',
--- building it for a @vs@ of given 'Len'.
-readTyName ::
- Source src =>
- Name2Type src -> src -> Len vs -> NameTy ->
- Either (Error_Type src) (TypeT src vs)
-readTyName cs src len name =
-       case Map.lookup name cs of
-        Just (TypeTLen t) -> Right $ t len
-        Nothing -> Left $ Error_Type_Constant_unknown $ At src name
+                       Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y
 
 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
 readVars :: Source src => EVars src -> AST_Type src -> EVars src
@@ -74,48 +55,3 @@ readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
 readVars evs BinTree0{} = evs
 readVars evs (BinTree2 x y) =
        readVars (readVars evs x) y
-
--- * Type 'Name2Type'
-type Name2Type src = Map NameTy (TypeTLen src)
-
--- ** Type 'TypeTLen'
--- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
---
--- Useful to build a 'Name2Type' which can be used
--- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
-newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)
-instance Source src => Eq (TypeTLen src) where
-       TypeTLen x == TypeTLen y = x LenZ == y LenZ
-instance Source src => Show (TypeTLen src) where
-       showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
-
--- ** Class 'Inj_Name2Type'
--- | Derive a 'Name2Type' from the given type-level list
--- of 'Proxy'-fied /type constants/.
-class Inj_Name2Type cs where
-       inj_Name2Type :: Source src => Name2Type src
-instance Inj_Name2Type '[] where
-       inj_Name2Type = Map.empty
-instance
- ( Inj_KindP (Ty_of_Type (K c))
- , K c ~ Type_of_Ty (Ty_of_Type (K c))
- , Constable c
- , Inj_Name2Type cs
- ) => Inj_Name2Type (Proxy c ': cs) where
-       inj_Name2Type =
-               Map.insert
-                (NameTy $ Text.pack $ show $ typeRep (Proxy @c))
-                (TypeTLen $ \len -> TypeT $ TyConst noSource len $
-                       inj_ConstKi @(K c) @c $
-                       inj_KindP @(Ty_of_Type (K c)) noSource) $
-               inj_Name2Type @cs
-
--- * Type 'Error_Type'
-data Error_Type src
- =   Error_Type_Constant_unknown (At src NameTy)
- |   Error_Type_Con_Kind         (Con_Kind src)
- deriving (Eq, Show)
-instance Inj_Error (Error_Type src) (Error_Type src) where
-       inj_Error = id
-instance Inj_Error (Con_Kind src) (Error_Type src) where
-       inj_Error = Error_Type_Con_Kind