{-# LANGUAGE PatternGuards #-}
----------------------------------------------------------------------
-- |
-- Module      : Optimize
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/09/16 13:56:13 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.18 $
--
-- Top-level partial evaluation for GF source modules.
-----------------------------------------------------------------------------

module GF.Compile.Optimize (optimizeModule) where

import GF.Grammar.Grammar
import GF.Infra.Ident
import GF.Grammar.Printer
import GF.Grammar.Macros
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
import GF.Data.Operations
import GF.Infra.Option

import Control.Monad
import qualified Data.Set as Set
import qualified Data.Map as Map
import GF.Text.Pretty
import Debug.Trace

-- | partial evaluation of concrete syntax. AR 6\/2001 -- 16\/5\/2003 -- 5\/2\/2005.

optimizeModule :: Options -> SourceGrammar -> SourceModule -> Err SourceModule
optimizeModule :: Options -> SourceGrammar -> SourceModule -> Err SourceModule
optimizeModule Options
opts SourceGrammar
sgr m :: SourceModule
m@(ModuleName
name,ModuleInfo
mi)
  | ModuleInfo -> ModuleStatus
mstatus ModuleInfo
mi ModuleStatus -> ModuleStatus -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleStatus
MSComplete = do
      [(Ident, Info)]
ids <- SourceModule -> Err [(Ident, Info)]
forall (m :: * -> *).
ErrorMonad m =>
SourceModule -> m [(Ident, Info)]
topoSortJments SourceModule
m
      ModuleInfo
mi <- (ModuleInfo -> (Ident, Info) -> Err ModuleInfo)
-> ModuleInfo -> [(Ident, Info)] -> Err ModuleInfo
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ModuleInfo -> (Ident, Info) -> Err ModuleInfo
updateEvalInfo ModuleInfo
mi [(Ident, Info)]
ids
      SourceModule -> Err SourceModule
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName
name,ModuleInfo
mi)
  | Bool
otherwise = SourceModule -> Err SourceModule
forall (m :: * -> *) a. Monad m => a -> m a
return SourceModule
m
 where
   oopts :: Options
oopts = Options
opts Options -> Options -> Options
`addOptions` ModuleInfo -> Options
mflags ModuleInfo
mi

   resenv :: GlobalEnv
resenv = Options -> SourceGrammar -> GlobalEnv
resourceValues Options
oopts SourceGrammar
sgr

   updateEvalInfo :: ModuleInfo -> (Ident, Info) -> Err ModuleInfo
updateEvalInfo ModuleInfo
mi (Ident
i,Info
info) = do
     Info
info <- Options
-> GlobalEnv
-> SourceGrammar
-> SourceModule
-> Ident
-> Info
-> Err Info
evalInfo Options
oopts GlobalEnv
resenv SourceGrammar
sgr (ModuleName
name,ModuleInfo
mi) Ident
i Info
info
     ModuleInfo -> Err ModuleInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo
mi{jments :: Map Ident Info
jments=Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
i Info
info (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)})

evalInfo :: Options -> GlobalEnv -> SourceGrammar -> SourceModule -> Ident -> Info -> Err Info
evalInfo :: Options
-> GlobalEnv
-> SourceGrammar
-> SourceModule
-> Ident
-> Info
-> Err Info
evalInfo Options
opts GlobalEnv
resenv SourceGrammar
sgr SourceModule
m Ident
c Info
info = do

 (if Options -> Verbosity -> Bool
verbAtLeast Options
opts Verbosity
Verbose then String -> (() -> Err ()) -> () -> Err ()
forall a. String -> a -> a
trace (String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ident -> String
showIdent Ident
c) else (() -> Err ()) -> () -> Err ()
forall a. a -> a
id) () -> Err ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

 String -> Err Info -> Err Info
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (String
"optimizing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ident -> String
showIdent Ident
c) (Err Info -> Err Info) -> Err Info -> Err Info
forall a b. (a -> b) -> a -> b
$ case Info
info of

  CncCat Maybe (L Type)
ptyp Maybe (L Type)
pde Maybe (L Type)
pre Maybe (L Type)
ppr Maybe PMCFG
mpmcfg -> do
    Maybe (L Type)
pde' <- case (Maybe (L Type)
ptyp,Maybe (L Type)
pde) of
      (Just (L Location
_ Type
typ), Just (L Location
loc Type
de)) -> do
        Type
de <- Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
partEval Options
opts SourceGrammar
gr ([(BindType
Explicit, Ident
varStr, Type
typeStr)], Type
typ) Type
de
        Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc (Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
0 Type
de)))
      (Just (L Location
loc Type
typ), Maybe (L Type)
Nothing) -> do
        Type
de <- SourceGrammar -> Type -> Err Type
mkLinDefault SourceGrammar
gr Type
typ
        Type
de <- Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
partEval Options
opts SourceGrammar
gr ([(BindType
Explicit, Ident
varStr, Type
typeStr)], Type
typ) Type
de
        Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc (Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
0 Type
de)))
      (Maybe (L Type), Maybe (L Type))
_ -> Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
pde   -- indirection

    Maybe (L Type)
pre' <- case (Maybe (L Type)
ptyp,Maybe (L Type)
pre) of
      (Just (L Location
_ Type
typ), Just (L Location
loc Type
re)) -> do
        Type
re <- Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
partEval Options
opts SourceGrammar
gr ([(BindType
Explicit, Ident
varStr, Type
typ)], Type
typeStr) Type
re
        Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc (Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
0 Type
re)))
      (Just (L Location
loc Type
typ), Maybe (L Type)
Nothing) -> do
        Type
re <- SourceGrammar -> Type -> Err Type
mkLinReference SourceGrammar
gr Type
typ
        Type
re <- Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
partEval Options
opts SourceGrammar
gr ([(BindType
Explicit, Ident
varStr, Type
typ)], Type
typeStr) Type
re
        Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc (Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
0 Type
re)))
      (Maybe (L Type), Maybe (L Type))
_ -> Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
pre   -- indirection

    let ppr' :: Maybe (L Type)
ppr' = (L Type -> L Type) -> Maybe (L Type) -> Maybe (L Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GlobalEnv -> Ident -> L Type -> L Type
evalPrintname GlobalEnv
resenv Ident
c) Maybe (L Type)
ppr

    Info -> Err Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe PMCFG
-> Info
CncCat Maybe (L Type)
ptyp Maybe (L Type)
pde' Maybe (L Type)
pre' Maybe (L Type)
ppr' Maybe PMCFG
mpmcfg)

  CncFun (mt :: Maybe (Ident, Context, Type)
mt@(Just (Ident
_,Context
cont,Type
val))) Maybe (L Type)
pde Maybe (L Type)
ppr Maybe PMCFG
mpmcfg -> --trace (prt c) $
       Doc -> Err Info -> Err Info
forall (m :: * -> *) a2 a.
(ErrorMonad m, Pretty a2) =>
a2 -> m a -> m a
eIn (String
"linearization in type" String -> Type -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Context -> Type -> [Type] -> Type
mkProd Context
cont Type
val [] Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ String
"of function") (Err Info -> Err Info) -> Err Info -> Err Info
forall a b. (a -> b) -> a -> b
$ do
    Maybe (L Type)
pde' <- case Maybe (L Type)
pde of
      Just (L Location
loc Type
de) -> do Type
de <- Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
partEval Options
opts SourceGrammar
gr (Context
cont,Type
val) Type
de
                            Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc (Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
0 Type
de)))
      Maybe (L Type)
Nothing -> Maybe (L Type) -> Err (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
pde
    let ppr' :: Maybe (L Type)
ppr' = (L Type -> L Type) -> Maybe (L Type) -> Maybe (L Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GlobalEnv -> Ident -> L Type -> L Type
evalPrintname GlobalEnv
resenv Ident
c) Maybe (L Type)
ppr
    Info -> Err Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Info -> Err Info) -> Info -> Err Info
forall a b. (a -> b) -> a -> b
$ Maybe (Ident, Context, Type)
-> Maybe (L Type) -> Maybe (L Type) -> Maybe PMCFG -> Info
CncFun Maybe (Ident, Context, Type)
mt Maybe (L Type)
pde' Maybe (L Type)
ppr' Maybe PMCFG
mpmcfg -- only cat in type actually needed
{-
  ResOper pty pde
    | not new && OptExpand `Set.member` optim -> do
         pde' <- case pde of
                   Just (L loc de) -> do de <- computeConcrete gr de
                                         return (Just (L loc (factor param c 0 de)))
                   Nothing -> return Nothing
         return $ ResOper pty pde'
-}
  Info
_ ->  Info -> Err Info
forall (m :: * -> *) a. Monad m => a -> m a
return Info
info
 where
-- new = flag optNewComp opts -- computations moved to GF.Compile.GeneratePMCFG

   gr :: SourceGrammar
gr = SourceGrammar -> SourceModule -> SourceGrammar
prependModule SourceGrammar
sgr SourceModule
m
   optim :: Set Optimization
optim = (Flags -> Set Optimization) -> Options -> Set Optimization
forall a. (Flags -> a) -> Options -> a
flag Flags -> Set Optimization
optOptimizations Options
opts
   param :: Bool
param = Optimization
OptParametrize Optimization -> Set Optimization -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Optimization
optim
   eIn :: a2 -> m a -> m a
eIn a2
cat = String -> m a -> m a
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (Doc -> String
forall a. Pretty a => a -> String
render (String
"Error optimizing" String -> a2 -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> a2
cat Doc -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c Doc -> Char -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Char
':'))

-- | the main function for compiling linearizations
partEval :: Options -> SourceGrammar -> (Context,Type) -> Term -> Err Term
partEval :: Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
partEval Options
opts = {-if flag optNewComp opts
                then-} Options -> SourceGrammar -> (Context, Type) -> Type -> Err Type
forall (m :: * -> *) p p a b.
(ErrorMonad m, MonadFail m) =>
p -> p -> (a, b) -> Type -> m Type
partEvalNew Options
opts
                {-else partEvalOld opts-}

partEvalNew :: p -> p -> (a, b) -> Type -> m Type
partEvalNew p
opts p
gr (a
context, b
val) Type
trm =
    String -> m Type -> m Type
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (Doc -> String
forall a. Pretty a => a -> String
render (String
"partial evaluation" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
trm)) (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$
    Type -> m Type
forall (m :: * -> *). MonadFail m => Type -> m Type
checkPredefError Type
trm
{-
partEvalOld opts gr (context, val) trm = errIn (render (text "partial evaluation" <+> ppTerm Qualified 0 trm)) $ do
  let vars  = map (\(bt,x,t) -> x) context
      args  = map Vr vars
      subst = [(v, Vr v) | v <- vars]
      trm1 = mkApp trm args
  trm2 <- computeTerm gr subst trm1
  trm3 <- if rightType trm2
          then computeTerm gr subst trm2 -- compute twice??
          else recordExpand val trm2 >>= computeTerm gr subst
  trm4 <- checkPredefError trm3
  return $ mkAbs [(Explicit,v) | v <- vars] trm4
  where
    -- don't eta expand records of right length (correct by type checking)
    rightType (R rs) = case val of
                         RecType ts -> length rs == length ts
                         _          -> False
    rightType _      = False


-- here we must be careful not to reduce
--   variants {{s = "Auto" ; g = N} ; {s = "Wagen" ; g = M}}
--   {s  = variants {"Auto" ; "Wagen"} ; g  = variants {N ; M}} ;

recordExpand :: Type -> Term -> Err Term
recordExpand typ trm = case typ of
  RecType tys -> case trm of
    FV rs -> return $ FV [R [assign lab (P r lab) | (lab,_) <- tys] | r <- rs]
    _ -> return $ R [assign lab (P trm lab) | (lab,_) <- tys]
  _ -> return trm

-}
-- | auxiliaries for compiling the resource

mkLinDefault :: SourceGrammar -> Type -> Err Term
mkLinDefault :: SourceGrammar -> Type -> Err Type
mkLinDefault SourceGrammar
gr Type
typ = (Type -> Type) -> Err Type -> Err Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (BindType -> Ident -> Type -> Type
Abs BindType
Explicit Ident
varStr) (Err Type -> Err Type) -> Err Type -> Err Type
forall a b. (a -> b) -> a -> b
$ Type -> Err Type
mkDefField Type
typ
 where
   mkDefField :: Type -> Err Type
mkDefField Type
typ = case Type
typ of
     Table Type
p Type
t  -> do
       Type
t' <- Type -> Err Type
mkDefField Type
t
       let T TInfo
_ [Case]
cs = Type -> Type
mkWildCases Type
t'
       Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Err Type) -> Type -> Err Type
forall a b. (a -> b) -> a -> b
$ TInfo -> [Case] -> Type
T (Type -> TInfo
TWild Type
p) [Case]
cs
     Sort Ident
s | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cStr -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Err Type) -> Type -> Err Type
forall a b. (a -> b) -> a -> b
$ Ident -> Type
Vr Ident
varStr
     QC QIdent
p           -> do [Type]
vs <- SourceGrammar -> QIdent -> Err [Type]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> QIdent -> m [Type]
lookupParamValues SourceGrammar
gr QIdent
p
                          case [Type]
vs of
                            Type
v:[Type]
_ -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
v
                            [Type]
_   -> String -> Err Type
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"no parameter values given to type" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> QIdent -> Doc
ppQIdent TermPrintQual
Qualified QIdent
p))
     RecType [Labelling]
r  -> do
       let ([Label]
ls,[Type]
ts) = [Labelling] -> ([Label], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip [Labelling]
r
       [Type]
ts <- (Type -> Err Type) -> [Type] -> Err [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Err Type
mkDefField [Type]
ts
       Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Err Type) -> Type -> Err Type
forall a b. (a -> b) -> a -> b
$ [Assign] -> Type
R ((Label -> Type -> Assign) -> [Label] -> [Type] -> [Assign]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Label -> Type -> Assign
assign [Label]
ls [Type]
ts)
     Type
_ | Just Int
_ <- Type -> Maybe Int
isTypeInts Type
typ -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Err Type) -> Type -> Err Type
forall a b. (a -> b) -> a -> b
$ Int -> Type
EInt Int
0 -- exists in all as first val
     Type
_ -> String -> Err Type
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"linearization type field cannot be" String -> Type -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type
typ))

mkLinReference :: SourceGrammar -> Type -> Err Term
mkLinReference :: SourceGrammar -> Type -> Err Type
mkLinReference SourceGrammar
gr Type
typ =
 (Type -> Type) -> Err Type -> Err Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (BindType -> Ident -> Type -> Type
Abs BindType
Explicit Ident
varStr) (Err Type -> Err Type) -> Err Type -> Err Type
forall a b. (a -> b) -> a -> b
$
   case Type -> Type -> Err Type
mkDefField Type
typ (Ident -> Type
Vr Ident
varStr) of
     Bad String
"no string" -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
Empty
     Err Type
x               -> Err Type
x
 where
   mkDefField :: Type -> Type -> Err Type
mkDefField Type
ty Type
trm =
     case Type
ty of
       Table Type
pty Type
ty -> do [Type]
ps <- SourceGrammar -> Type -> Err [Type]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> Type -> m [Type]
allParamValues SourceGrammar
gr Type
pty
                          case [Type]
ps of
                            []     -> String -> Err Type
forall a. String -> Err a
Bad String
"no string"
                            (Type
p:[Type]
ps) -> Type -> Type -> Err Type
mkDefField Type
ty (Type -> Type -> Type
S Type
trm Type
p)
       Sort Ident
s | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cStr -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
trm
       QC QIdent
p       -> String -> Err Type
forall a. String -> Err a
Bad String
"no string"
       RecType [] -> String -> Err Type
forall a. String -> Err a
Bad String
"no string"
       RecType [Labelling]
rs -> do
         [Err Type] -> Err Type
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ((Labelling -> Err Type) -> [Labelling] -> [Err Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(Label
l,Type
ty) -> Type -> Type -> Err Type
mkDefField Type
ty (Type -> Label -> Type
P Type
trm Label
l)) ([Labelling] -> [Labelling]
forall a. [(Label, a)] -> [(Label, a)]
sortRec [Labelling]
rs))
           Err Type -> Err Type -> Err Type
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` String -> Err Type
forall a. String -> Err a
Bad String
"no string"
       Type
_ | Just Int
_ <- Type -> Maybe Int
isTypeInts Type
typ -> String -> Err Type
forall a. String -> Err a
Bad String
"no string"
       Type
_ -> String -> Err Type
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"linearization type field cannot be" String -> Type -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type
typ))

evalPrintname :: GlobalEnv -> Ident -> L Term -> L Term
evalPrintname :: GlobalEnv -> Ident -> L Type -> L Type
evalPrintname GlobalEnv
resenv Ident
c (L Location
loc Type
pr) = Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc (GlobalEnv -> L Ident -> Type -> Type
normalForm GlobalEnv
resenv (Location -> Ident -> L Ident
forall a. Location -> a -> L a
L Location
loc Ident
c) Type
pr)

-- do even more: factor parametric branches

factor :: Bool -> Ident -> Int -> Term -> Term
factor :: Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
i Type
t =
  case Type
t of
    T (TComp Type
ty) [Case]
cs -> Type -> [Case] -> Type
factors Type
ty [(Patt
p, Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Type
v) | (Patt
p, Type
v) <- [Case]
cs]
    Type
_               -> (Type -> Type) -> Type -> Type
composSafeOp (Bool -> Ident -> Int -> Type -> Type
factor Bool
param Ident
c Int
i) Type
t
  where
    factors :: Type -> [Case] -> Type
factors Type
ty [Case]
pvs0
                 | Bool -> Bool
not Bool
param = Type -> [Type] -> Type
V Type
ty ((Case -> Type) -> [Case] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Case -> Type
forall a b. (a, b) -> b
snd [Case]
pvs0)
    factors Type
ty []            = Type -> [Type] -> Type
V Type
ty []
    factors Type
ty pvs0 :: [Case]
pvs0@[(Patt
p,Type
v)]  = Type -> [Type] -> Type
V Type
ty [Type
v]
    factors Type
ty pvs0 :: [Case]
pvs0@(Case
pv:[Case]
pvs) =
      let t :: Type
t  = Case -> Type
mkFun Case
pv
          ts :: [Type]
ts = (Case -> Type) -> [Case] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Case -> Type
mkFun [Case]
pvs
      in if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
==Type
t) [Type]
ts
           then TInfo -> [Case] -> Type
T (Type -> TInfo
TTyped Type
ty) (Type -> [Case]
forall b. b -> [(Patt, b)]
mkCases Type
t)
           else Type -> [Type] -> Type
V Type
ty ((Case -> Type) -> [Case] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Case -> Type
forall a b. (a, b) -> b
snd [Case]
pvs0)

    --- we hope this will be fresh and don't check... in GFC would be safe
    qvar :: Ident
qvar = String -> Ident
identS (String
"q_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ident -> String
showIdent Ident
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"__" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)

    mkFun :: Case -> Type
mkFun (Patt
patt, Type
val) = Type -> Type -> Type -> Type
replace (Patt -> Type
patt2term Patt
patt) (Ident -> Type
Vr Ident
qvar) Type
val
    mkCases :: b -> [(Patt, b)]
mkCases b
t = [(Ident -> Patt
PV Ident
qvar, b
t)]

--  we need to replace subterms
replace :: Term -> Term -> Term -> Term
replace :: Type -> Type -> Type -> Type
replace Type
old Type
new Type
trm =
  case Type
trm of
    -- these are the important cases, since they can correspond to patterns
    QC QIdent
_     | Type
trm Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
old -> Type
new
    App Type
_ Type
_  | Type
trm Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
old -> Type
new
    R [Assign]
_      | Type
trm Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
old -> Type
new
    App Type
x Type
y               -> Type -> Type -> Type
App (Type -> Type -> Type -> Type
replace Type
old Type
new Type
x) (Type -> Type -> Type -> Type
replace Type
old Type
new Type
y)
    Type
_                     -> (Type -> Type) -> Type -> Type
composSafeOp (Type -> Type -> Type -> Type
replace Type
old Type
new) Type
trm