Remove debugging entry map_f.

[haskell/symantic.git] / symantic / Language / Symantic / Compiling / Term.hs

diff --git a/symantic/Language/Symantic/Compiling/Term.hs b/symantic/Language/Symantic/Compiling/Term.hs
index f587e06386837fd2c29adcd5fd124e0fd383b340..1dc2b8ce7ac24cf9ed0cdb06248270d6287ddf18 100644 (file)
--- a/symantic/Language/Symantic/Compiling/Term.hs
+++ b/symantic/Language/Symantic/Compiling/Term.hs
@@ -20,8 +20,8 @@ import Language.Symantic.Typing
 
 -- * Type 'Term'
 data Term src ss ts vs (t::K.Type)
- =   Term (Type src vs (QualOf t::K.Constraint))
-          (Type src vs (UnQualOf t::K.Type))
+ =   Term (Type src vs (QualOf t))
+          (Type src vs (UnQualOf t))
           (TeSym ss ts t)
 instance Source src => Eq (Term src ss ts vs t) where
        Term qx tx _ == Term qy ty _ = qx == qy && tx == ty
@@ -65,20 +65,29 @@ instance Source src => Eq (TermVT src ss ts) where
                isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
 instance Source src => Show (TermVT src ss ts) where
        showsPrec p (TermVT t) = showsPrec p t
+type instance SourceOf (TermVT src ss ts) = src
+instance Source src => Sourced (TermVT src ss ts) where
+       sourceOf  (TermVT t)     = sourceOf t
+       setSource (TermVT t) src = TermVT $ setSource t src
 
--- ** Type 'TermVT_CF'
+liftTermVT :: TermVT src ss '[] -> TermVT src ss ts
+liftTermVT (TermVT (Term q t (TeSym te))) =
+       TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
+       TeSym $ \_c -> te CtxTeZ
+
+-- ** Type 'TermAVT'
 -- | Like 'TermVT', but 'CtxTe'-free.
-data TermVT_CF src ss = forall vs t. TermVT_CF (forall ts. Term src ss ts vs t)
-type instance SourceOf (TermVT_CF src ss) = src
-instance Source src => Sourced (TermVT_CF src ss) where
-       sourceOf  (TermVT_CF t)     = sourceOf t
-       setSource (TermVT_CF t) src = TermVT_CF (setSource t src)
-instance Source src => Eq (TermVT_CF src ss) where
-       TermVT_CF x == TermVT_CF y =
+data TermAVT src ss = forall vs t. TermAVT (forall ts. Term src ss ts vs t)
+type instance SourceOf (TermAVT src ss) = src
+instance Source src => Sourced (TermAVT src ss) where
+       sourceOf  (TermAVT t)     = sourceOf t
+       setSource (TermAVT t) src = TermAVT (setSource t src)
+instance Source src => Eq (TermAVT src ss) where
+       TermAVT x == TermAVT y =
                let (Term qx' tx' _, Term qy' ty' _) = appendVars x y in
                isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
-instance Source src => Show (TermVT_CF src ss) where
-       showsPrec p (TermVT_CF t) = showsPrec p t
+instance Source src => Show (TermAVT src ss) where
+       showsPrec p (TermAVT t) = showsPrec p t
 
 -- * Type 'TeSym'
 -- | Symantic of a 'Term'.
@@ -101,11 +110,13 @@ teSym ::
 teSym t = inj_Sym @s (TeSym $ const t)
 
 -- ** Type family 'QualOf'
+-- | Qualification
 type family QualOf (t::K.Type) :: Constraint where
        QualOf (q #> t) = q -- (q # QualOf t)
        QualOf t = (()::Constraint)
 
 -- ** Type family 'UnQualOf'
+-- | Unqualification
 type family UnQualOf (t::K.Type) :: K.Type where
        UnQualOf (q #> t) = t -- UnQualOf t
        UnQualOf t = t
@@ -210,6 +221,13 @@ class Sym_Lambda term where
        lam1 :: (term a -> term b) -> term (a -> b)
        default lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b)
        lam1 = lam
+       
+       -- | /Qualification/.
+       --
+       -- Workaround used in 'readTermWithCtx'.
+       qual :: proxy q -> term t -> term (q #> t)
+       default qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t)
+       qual q = trans1 (qual q)
 
 lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c)
 lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d)
@@ -224,7 +242,8 @@ instance Sym_Lambda Eval where
        app    = (<*>)
        lam f  = Eval (unEval . f . Eval)
        lam1   = lam
-       let_ x f = f x -- like flip ($)
+       qual _q (Eval t) = Eval $ Qual t
+       let_ x f = f x -- NOTE: like flip ($)
 instance Sym_Lambda View where
        apply = View $ \_po _v -> "($)"
        app (View a1) (View a2) = View $ \po v ->
@@ -238,6 +257,7 @@ instance Sym_Lambda View where
                unView (f (View $ \_po _v -> x)) (op, SideL) (succ v)
                where op = infixN 1
        lam1 = lam
+       qual _q (View t) = View t -- TODO: maybe print q
        let_ x f =
                View $ \po v ->
                        let x' = "x" <> Text.pack (show v) in
@@ -252,3 +272,4 @@ instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2) where
        lam f = dup_1 lam_f `Dup` dup_2 lam_f
                where lam_f = lam f
        lam1 = lam
+       qual q = dup1 @Sym_Lambda (qual q)