Fix breakableFill: do not impose alignment.

[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 3efbc96bfbe1b444c45e24832e2e8a1394470f90..3b2da6186962e5dd35a67f01dd45b64a87de29b8 100644 (file)
--- a/symantic/Language/Symantic/Compiling/Term.hs
+++ b/symantic/Language/Symantic/Compiling/Term.hs
@@ -52,8 +52,8 @@ instance ExpandFam (Term src ss ts vs t) where
        expandFam (Term q t te) = Term (expandFam q) (expandFam t) te
 
 -- Type
-instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
-       typeOf t = typeOfTerm t `source` TermT t
+instance SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
+       typeOf t = typeOfTerm t `withSource` TermT t
 
 typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
 typeOfTerm (Term q t _) = q #> t
@@ -111,13 +111,13 @@ newtype TeSym ss ts (t::K.Type)
  )
 
 -- | Like 'TeSym', but 'CtxTe'-free
--- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.
+-- and using 'symInj' to be able to use 'Sym'@ s@ inside.
 teSym ::
  forall s ss ts t.
- Inj_Sym ss s =>
- (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
+ SymInj ss s =>
+ (forall term. Sym s term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
  TeSym ss ts t
-teSym t = inj_Sym @s (TeSym $ const t)
+teSym t = symInj @s (TeSym $ const t)
 
 -- ** Type family 'QualOf'
 -- | Qualification
@@ -165,40 +165,40 @@ data CtxTe (term::K.Type -> K.Type) (hs::[K.Type]) where
 infixr 5 `CtxTeS`
 
 -- ** Type 'TermDef'
--- | Convenient type alias for defining 'Term'.
-type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t
+-- | Convenient type alias to define a 'Term'.
+type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
 
 -- ** Type family 'Sym'
-type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint
+type family Sym (s::k) :: {-term-}(K.Type -> K.Type) -> Constraint
 
 -- ** Type family 'Syms'
-type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where
+type family Syms (ss::[K.Type]) (term::K.Type -> K.Type) :: Constraint where
        Syms '[] term = ()
-       Syms (s ': ss) term = (Sym s term, Syms ss term)
+       Syms (Proxy s ': ss) term = (Sym s term, Syms ss term)
 
--- ** Type 'Inj_Sym'
--- | Convenient type synonym wrapping 'Inj_SymP'
+-- ** Type 'SymInj'
+-- | Convenient type synonym wrapping 'SymPInj'
 -- applied on the correct 'Index'.
-type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
+type SymInj ss s = SymInjP (Index ss (Proxy s)) ss s
 
 -- | Inject a given /symantic/ @s@ into a list of them,
 -- by returning a function which given a 'TeSym' on @s@
 -- returns the same 'TeSym' on @ss@.
-inj_Sym ::
+symInj ::
  forall s ss ts t.
- Inj_Sym ss s =>
+ SymInj ss s =>
  TeSym '[Proxy s] ts t ->
  TeSym ss ts t
-inj_Sym = inj_SymP (Proxy @(Index ss (Proxy s)))
+symInj = symInjP @(Index ss (Proxy s))
 
--- *** Class 'Inj_SymP'
-class Inj_SymP p ss s where
-       inj_SymP :: Proxy p -> TeSym '[Proxy s] ts t -> TeSym ss ts t
-instance Inj_SymP Zero (Proxy s ': ss) (s::k) where
-       inj_SymP _ = \(TeSym te) -> TeSym te
-instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where
-       inj_SymP _p = \(te::TeSym '[Proxy s] ts t) ->
-               case inj_SymP (Proxy @p) te :: TeSym ss ts t of
+-- *** Class 'SymPInj'
+class SymInjP p ss s where
+       symInjP :: TeSym '[Proxy s] ts t -> TeSym ss ts t
+instance SymInjP Zero (Proxy s ': ss) (s::k) where
+       symInjP (TeSym te) = TeSym te
+instance SymInjP p ss s => SymInjP (Succ p) (Proxy not_s ': ss) s where
+       symInjP (te::TeSym '[Proxy s] ts t) =
+               case symInjP @p te :: TeSym ss ts t of
                 TeSym te' -> TeSym te'
 
 -- * Class 'Sym_Lambda'