Rename Dim -> Dimension.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Ratio.hs
index 46ed41b119d71e1c3b95fbfca639e702f2217313..f09b8d38a82d1df11f8f38c141449c2890ecdfce 100644 (file)
@@ -11,7 +11,7 @@ import Language.Symantic.Lib.Function (a0)
 import Language.Symantic.Lib.Integral (tyIntegral)
 
 -- * Class 'Sym_Ratio'
-type instance Sym (Proxy Ratio) = Sym_Ratio
+type instance Sym Ratio = Sym_Ratio
 class Sym_Ratio term where
        ratio       :: Integral a => term a -> term a -> term (Ratio a)
        numerator   :: term (Ratio a) -> term a
@@ -43,15 +43,17 @@ instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (Dup r1 r2) where
 instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)
 
 -- Typing
+instance NameTyOf Ratio where
+       nameTyOf _c = ["Ratio"] `Mod` "Ratio"
 instance FixityOf Ratio
 instance ClassInstancesFor Ratio where
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@a)
         | Just HRefl <- proj_ConstKiTy @_ @Ratio c
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
                   | Just Refl <- proj_Const @Real q
                   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
@@ -68,7 +70,7 @@ instance TypeInstancesFor Ratio
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Ratio
-instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where
+instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where
        moduleFor = ["Ratio"] `moduleWhere`
         [ "ratio"       := teRatio
         , "numerator"   := teRatio_numerator