Fix breakableFill: do not impose alignment.

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

diff --git a/symantic/Language/Symantic/Compiling/Beta.hs b/symantic/Language/Symantic/Compiling/Beta.hs
index a0cd3bf809b4385395428e5b0265e9c44d38996a..5fa44a1e148c4067b6e5b92c657a772786687656 100644 (file)
--- a/symantic/Language/Symantic/Compiling/Beta.hs
+++ b/symantic/Language/Symantic/Compiling/Beta.hs
@@ -10,31 +10,40 @@ import Language.Symantic.Compiling.Term
 
 -- | Term application: apply second given 'TermT' to the first,
 -- applying embedded 'TeSym's, or return an error.
-betaTe ::
- forall src ss es vs fun arg.
- Inj_Source (TypeVT src) src =>
+betaTerm ::
+ forall src ss ts vs fun arg.
+ SourceInj (TypeVT src) src =>
  Constable (->) =>
- Term src ss es vs (fun::K.Type) ->
- Term src ss es vs (arg::K.Type) ->
- Either (Error_Beta src) (TermT src ss es vs)
-betaTe (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
+ Term src ss ts vs (fun::K.Type) ->
+ Term src ss ts vs (arg::K.Type) ->
+ Either (Error_Beta src) (TermT src ss ts vs)
+betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
        case tf of
         TyApp _ (TyApp _ a2b a2b_a) a2b_b
          | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->
-               case a2b_a `eqTy` ta of
+               case a2b_a `eqType` ta of
                 Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
                 Just Refl ->
-                       Right $ TermT $ Term @_ @_ @_ @_ @(_ #> _) (qf # qa) a2b_b
-                        (TeSym $ \c -> te_fun c `app` te_arg c)
+                       Right $
+                       case (proveConstraint qf, proveConstraint qa) of
+                        -- NOTE: remove provable Constraints to keep those smaller.
+                        (Just Dict, Just Dict) -> TermT $ Term (noConstraintLen (lenVars a2b_b)) a2b_b $
+                               TeSym $ \c -> te_fun c `app` te_arg c
+                        (Just Dict, Nothing) -> TermT $ Term qa a2b_b $
+                               TeSym $ \c -> te_fun c `app` te_arg c
+                        (Nothing, Just Dict) -> TermT $ Term qf a2b_b $
+                               TeSym $ \c -> te_fun c `app` te_arg c
+                        (Nothing, Nothing) -> TermT $ Term (qf # qa) a2b_b $
+                               TeSym $ \c -> te_fun c `app` te_arg c
         _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf)
 
 -- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible.
-betasTe ::
- Inj_Source (TypeVT src) src =>
+betaTerms ::
+ SourceInj (TypeVT src) src =>
  Constable (->) =>
- BinTree (TermVT src ss es) ->
- Either (Error_Beta src) (TermVT src ss es)
-betasTe t =
+ BinTree (TermVT src ss ts) ->
+ Either (Error_Beta src) (TermVT src ss ts)
+betaTerms t =
        collapseBT (\acc ele -> do
                TermVT (Term qf tf te_fun) <- acc
                TermVT (Term qa ta te_arg) <- ele
@@ -46,14 +55,16 @@ betasTe t =
                        mgu <-
                                (Error_Beta_Unify `left`) $
                                case (unQualsTy af, unQualsTy ta') of
-                                (TypeK af', TypeK ta'') -> mguTy mempty af' ta''
+                                (TypeK af', TypeK ta'') -> unifyType mempty af' ta''
                        let qf'' = subst mgu qf'
                        let qa'' = subst mgu qa'
                        let tf'' = subst mgu tf'
                        let ta'' = subst mgu ta'
-                       TermT (Term qr tr te_res) <- betaTe (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
-                       normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->
+                       TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
+                       normalizeVarsTy (qr #> tr) $ \case
+                        TyApp _ (TyApp _ _c qr') tr' ->
                                Right $ TermVT $ Term qr' tr' te_res
+                        _ -> undefined -- FIXME: as of GHC 8.2, GHC is no longer clever enough to rule out other cases
         ) (Right <$> t)
 
 -- * Type 'Error_Beta'
@@ -65,14 +76,7 @@ data Error_Beta src
      -- with the 'Type' of the argument.
  deriving (Eq, Show)
 
-instance Inj_Error (Error_Beta src) (Error_Beta src) where
-       inj_Error = id
-instance Inj_Error (Error_Unify src) (Error_Beta src) where
-       inj_Error = Error_Beta_Unify
-
-{-
-(<<*>>) :: Monad m => m (a -> m b) -> m a -> m b
-(<<*>>) f a = f >>= (a >>=)
-infixl 4 <<*>>
-{-# INLINE (<<*>>) #-}
--}
+instance ErrorInj (Error_Beta src) (Error_Beta src) where
+       errorInj = id
+instance ErrorInj (Error_Unify src) (Error_Beta src) where
+       errorInj = Error_Beta_Unify