Add common instances to Interpreting.Dup.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Int.hs

diff --git a/symantic-lib/Language/Symantic/Lib/Int.hs b/symantic-lib/Language/Symantic/Lib/Int.hs
index 3f9cf06225798fc78c36ccea3617b38aac941d2a..ae9130434b81d962ff4808de86b0f7b57a6bbf6d 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Int.hs
+++ b/symantic-lib/Language/Symantic/Lib/Int.hs
@@ -3,12 +3,19 @@
 -- | Symantic for 'Int'.
 module Language.Symantic.Lib.Int where
 
+import Data.Eq (Eq)
+import Data.Function (($), (.))
+import Data.Int (Int)
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord)
+import Prelude (Bounded, Enum, Integral, Num, Real)
+import Text.Show (Show(..))
 import qualified Data.Text as Text
 
 import Language.Symantic
 
 -- * Class 'Sym_Int'
-type instance Sym (Proxy Int) = Sym_Int
+type instance Sym Int = Sym_Int
 class Sym_Int term where
        int :: Int -> term Int
        default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
@@ -27,8 +34,10 @@ instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where
 instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
 
 -- Typing
+instance NameTyOf Int where
+       nameTyOf _c = ["Int"] `Mod` "Int"
 instance ClassInstancesFor Int where
-       proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
+       proveConstraintFor _c (TyConst _ _ q :$ z)
         | Just HRefl <- proj_ConstKiTy @_ @Int z
         = case () of
                 _ | Just Refl <- proj_Const @Bounded  q -> Just Dict
@@ -45,12 +54,12 @@ instance TypeInstancesFor Int
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Int
-instance Module src ss Int
+instance ModuleFor src ss Int
 
 -- ** 'Type's
-tyInt :: Source src => Inj_Len vs => Type src vs Int
+tyInt :: Source src => LenInj vs => Type src vs Int
 tyInt = tyConst @(K Int) @Int
 
 -- ** 'Term's
-teInt :: Source src => Inj_Sym ss Int => Int -> Term src ss ts '[] Int
+teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
 teInt i = Term noConstraint tyInt $ teSym @Int $ int i