stack: bump to lts-12.25

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

diff --git a/symantic-lib/Language/Symantic/Lib/Ratio.hs b/symantic-lib/Language/Symantic/Lib/Ratio.hs
index d63831d4295fd116450023d2fab9ba26e6ea8301..09a259db2a347672bd1ceee22c8c581cda231a40 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Ratio.hs
+++ b/symantic-lib/Language/Symantic/Lib/Ratio.hs
@@ -3,7 +3,13 @@
 -- | Symantic for 'Ratio'.
 module Language.Symantic.Lib.Ratio where
 
+import Data.Eq (Eq)
+import Data.Function (($))
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord)
 import Data.Ratio (Ratio)
+import Prelude (Fractional, Integral, Num, Real, RealFrac)
+import Text.Show (Show)
 import qualified Data.Ratio as Ratio
 
 import Language.Symantic
@@ -11,7 +17,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 +49,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,8 +76,8 @@ instance TypeInstancesFor Ratio
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Ratio
-instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where
-       moduleFor _s = ["Ratio"] `moduleWhere`
+instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where
+       moduleFor = ["Ratio"] `moduleWhere`
         [ "ratio"       := teRatio
         , "numerator"   := teRatio_numerator
         , "denominator" := teRatio_denominator
@@ -83,6 +91,6 @@ tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a
 teRatio :: TermDef Ratio '[Proxy a] (Integral a #> (a -> a -> Ratio a))
 teRatio = Term (tyIntegral a0) (a0 ~> a0 ~> tyRatio a0) $ teSym @Ratio $ lam2 ratio
 
-teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (Ratio a -> a)
+teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (() #> (Ratio a -> a))
 teRatio_numerator   = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 numerator
 teRatio_denominator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 denominator