Add indent.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Function.hs b/symantic-lib/Language/Symantic/Lib/Function.hs
index 0f77afbf7b461071ca8c0f2408abd81c2a597c9f..f37a9a056f2dd637da2dd9803b94f30938252881 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Function.hs
+++ b/symantic-lib/Language/Symantic/Lib/Function.hs
@@ -10,7 +10,7 @@ import qualified Data.MonoTraversable as MT
 import Language.Symantic
 
 -- * Class 'Sym_Function'
-type instance Sym (Proxy (->)) = Sym_Function
+type instance Sym (->) = Sym_Function
 class Sym_Function term where
        comp  :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp`
        const :: term a -> term b -> term a
@@ -46,48 +46,50 @@ instance (Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2) where
 instance (Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)
 
 -- Typing
+instance NameTyOf (->) where
+       nameTyOf _c = [] `Mod` "->"
 instance ClassInstancesFor (->) where
-       proveConstraintFor _c (TyApp _ q (TyApp _ z _r))
-        | Just HRefl <- proj_ConstKiTy @_ @(->) z
+       proveConstraintFor _c (TyConst _ _ q :$ f:@_r)
+        | Just HRefl <- proj_ConstKiTy @_ @(->) f
         = case () of
-                _ | Just HRefl <- proj_ConstKiTy @_ @Functor     q -> Just Dict
-                  | Just HRefl <- proj_ConstKiTy @_ @Applicative q -> Just Dict
-                  | Just HRefl <- proj_ConstKiTy @_ @Monad       q -> Just Dict
+                _ | Just Refl <- proj_Const @Functor     q -> Just Dict
+                  | Just Refl <- proj_Const @Applicative q -> Just Dict
+                  | Just Refl <- proj_Const @Monad       q -> Just Dict
                 _ -> Nothing
-       proveConstraintFor _c (TyApp _ q (TyApp _ (TyApp _ z _a) b))
-        | Just HRefl <- proj_ConstKiTy @_ @(->) z
+       proveConstraintFor _c (tq@(TyConst _ _ q) :$ f:@_a:@b)
+        | Just HRefl <- proj_ConstKiTy @_ @(->) f
         = case () of
-                _ | Just HRefl <- proj_ConstKiTy @_ @Monoid q
-                  , Just Dict  <- proveConstraint (q `tyApp` b) -> Just Dict
-                  | Just HRefl <- proj_ConstKiTy @_ @MT.MonoFunctor q -> Just Dict
+                _ | Just Refl <- proj_Const @Monoid q
+                  , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
+                  | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor (->)
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g (->)
-instance (Source src, Inj_Sym ss (->)) => ModuleFor src ss (->) where
+instance (Source src, SymInj ss (->)) => ModuleFor src ss (->) where
        moduleFor = ["Function"] `moduleWhere`
         [ "const" := teFunction_const
         , "flip"  := teFunction_flip
         , "id"    := teFunction_id
         , "." `withInfixR` 9 := teFunction_compose
-        -- , "$" `withInfixR` 0 := teFunction_app
+        , "$" `withInfixR` 0 := teFunction_apply
         ]
 
 -- ** 'Type's
-tyFun :: Source src => Inj_Len vs => Type src vs (->)
+tyFun :: Source src => LenInj vs => Type src vs (->)
 tyFun = tyConst @(K (->)) @(->)
 
-a0 :: Source src => Inj_Len vs => Inj_Kind (K a) =>
+a0 :: Source src => LenInj vs => KindInj (K a) =>
      Type src (Proxy a ': vs) a
 a0 = tyVar "a" varZ
 
-b1 :: Source src => Inj_Len vs => Inj_Kind (K b) =>
+b1 :: Source src => LenInj vs => KindInj (K b) =>
      Type src (a ': Proxy b ': vs) b
 b1 = tyVar "b" $ VarS varZ
 
-c2 :: Source src => Inj_Len vs => Inj_Kind (K c) =>
+c2 :: Source src => LenInj vs => KindInj (K c) =>
      Type src (a ': b ': Proxy c ': vs) c
 c2 = tyVar "c" $ VarS $ VarS varZ
 
@@ -103,3 +105,6 @@ teFunction_flip = Term noConstraint ((a0 ~> b1 ~> c2) ~> (b1 ~> a0 ~> c2)) $ teS
 
 teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))
 teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id
+
+teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b))
+teFunction_apply = Term noConstraint ((a0 ~> b1) ~> a0 ~> b1) $ teSym @(->) apply