cdff1db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1659 from edwinb/partial-eval

More partial evaluation goodness

commitcdff1dbffa433d10a0146d3bb1f72be23aebbded authorEdwin Brady <edwin.brady@gmail.com> dateSat 18 Oct 2014, 22:33 (12 years ago) parentb0e1ecf 8e6b636

10 files changed+132−63

compare with master

unifiedsplit

src/IRTS/CodegenCommon.hs−1 src/IRTS/Compiler.hs+1−2 src/Idris/AbsSyntax.hs+50−18 src/Idris/AbsSyntaxTree.hs+12−5 src/Idris/CmdOptions.hs+3−1 src/Idris/Elab/Class.hs+1−1 src/Idris/Elab/Clause.hs+42−25 src/Idris/PartialEval.hs+8−5 src/Idris/REPL.hs+11−2 src/Idris/Transforms.hs+4−3

src/IRTS/CodegenCommon.hs−1

@@ -25,7 +25,6 @@ data CodegenInfo = CodegenInfo { outputFile :: String,

2525 outputType :: OutputType,

2626 targetTriple :: String,

2727 targetCPU :: String,

28− optimisation :: Word,

2928 includes :: [FilePath],

3029 importDirs :: [FilePath],

3130 compileObjs :: [String],

src/IRTS/Compiler.hs+1−2

@@ -89,11 +89,10 @@ compile codegen f tm

8989 Just f -> runIO $ writeFile f (dumpDefuns defuns)

9090 triple <- Idris.AbsSyntax.targetTriple

9191 cpu <- Idris.AbsSyntax.targetCPU

92− optimise <- optLevel

9392 iLOG "Building output"

9493

9594 case checked of

96− OK c -> do return $ CodegenInfo f outty triple cpu optimise

95+ OK c -> do return $ CodegenInfo f outty triple cpu

9796 hdrs impdirs objs libs flags

9897 NONE c (toAlist defuns)

9998 tagged

src/Idris/AbsSyntax.hs+50−18

@@ -608,13 +608,39 @@ logLevel = do i <- getIState

608608setErrContext :: Bool -> Idris ()

609609setErrContext t = do i <- getIState

610610 let opts = idris_options i

611− let opt' = opts { opt_errContext = t }

612− putIState $ i { idris_options = opt' }

611+ let opts' = opts { opt_errContext = t }

612+ putIState $ i { idris_options = opts' }

613613

614614errContext :: Idris Bool

615615errContext = do i <- getIState

616616 return (opt_errContext (idris_options i))

617617

618+getOptimise :: Idris [Optimisation]

619+getOptimise = do i <- getIState

620+ return (opt_optimise (idris_options i))

621+

622+setOptimise :: [Optimisation] -> Idris ()

623+setOptimise newopts = do i <- getIState

624+ let opts = idris_options i

625+ let opts' = opts { opt_optimise = newopts }

626+ putIState $ i { idris_options = opts' }

627+

628+addOptimise :: Optimisation -> Idris ()

629+addOptimise opt = do opts <- getOptimise

630+ setOptimise (nub (opt : opts))

631+

632+removeOptimise :: Optimisation -> Idris ()

633+removeOptimise opt = do opts <- getOptimise

634+ setOptimise ((nub opts) \\ [opt])

635+

636+-- Set appropriate optimisation set for the given level. We only have

637+-- one optimisation that is configurable at the moment, however!

638+setOptLevel :: Int -> Idris ()

639+setOptLevel n | n <= 0 = setOptimise []

640+setOptLevel 1 = setOptimise []

641+setOptLevel 2 = setOptimise [PETransform]

642+setOptLevel n | n >= 3 = setOptimise [PETransform]

643+

618644useREPL :: Idris Bool

619645useREPL = do i <- getIState

620646 return (opt_repl (idris_options i))

@@ -708,16 +734,6 @@ targetCPU :: Idris String

708734targetCPU = do i <- getIState

709735 return (opt_cpu (idris_options i))

710736

711−setOptLevel :: Word -> Idris ()

712−setOptLevel t = do i <- getIState

713− let opts = idris_options i

714− opt' = opts { opt_optLevel = t }

715− putIState $ i { idris_options = opt' }

716−

717−optLevel :: Idris Word

718−optLevel = do i <- getIState

719− return (opt_optLevel (idris_options i))

720−

721737verbose :: Idris Bool

722738verbose = do i <- getIState

723739 return (opt_verbose (idris_options i))

@@ -1059,12 +1075,14 @@ addStatics :: Name -> Term -> PTerm -> Idris ()

10591075addStatics n tm ptm =

10601076 do let (statics, dynamics) = initStatics tm ptm

10611077 ist <- getIState

1062− let paramnames = case lookupCtxtExact n (idris_fninfo ist) of

1063− Just p -> getNamesFrom 0 (fn_params p) tm

1064− _ -> []

1078+ let paramnames

1079+ = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1080+ Just p -> getNamesFrom 0 (fn_params p) tm ++

1081+ concatMap (getParamNames ist) (map snd statics)

1082+ _ -> concatMap (getParamNames ist) (map snd statics)

10651083

10661084 let stnames = nub $ concatMap freeArgNames (map snd statics)

1067− let dnames = nub $ concatMap freeArgNames (map snd dynamics)

1085+ let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

10681086 \\ paramnames

10691087 -- also get the arguments which are 'uniquely inferrable' from

10701088 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

@@ -1074,8 +1092,10 @@ addStatics n tm ptm =

10741092 let stpos = staticList statics' tm

10751093 i <- getIState

10761094 when (not (null statics)) $

1077− logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "

1078− ++ show statics' ++ "\n" ++ show dynamics

1095+ logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"

1096+ ++ showTmImpls ptm ++ "\n"

1097+ ++ show statics ++ "\n" ++ show dynamics

1098+ ++ "\n" ++ show paramnames

10791099 ++ "\n" ++ show stpos

10801100 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

10811101 addIBC (IBCStatic n)

@@ -1091,6 +1111,18 @@ addStatics n tm ptm =

10911111 else (static, dynamic)

10921112 initStatics t pt = ([], [])

10931113

1114+ getParamNames ist tm | (P _ n _ , args) <- unApply tm

1115+ = case lookupCtxtExact n (idris_datatypes ist) of

1116+ Just ti -> getNamePos 0 (param_pos ti) args

1117+ Nothing -> []

1118+ where getNamePos i ps [] = []

1119+ getNamePos i ps (P _ n _ : as)

1120+ | i `elem` ps = n : getNamePos (i + 1) ps as

1121+ getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1122+ getParamNames ist (Bind t (Pi (P _ n _) _) sc)

1123+ = n : getParamNames ist sc

1124+ getParamNames ist _ = []

1125+

10941126 getNamesFrom i ps (Bind n (Pi _ _) sc)

10951127 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

10961128 | otherwise = getNamesFrom (i + 1) ps sc

src/Idris/AbsSyntaxTree.hs+12−5

@@ -75,11 +75,11 @@ data IOption = IOption { opt_logLevel :: Int,

7575 opt_importdirs :: [FilePath],

7676 opt_triple :: String,

7777 opt_cpu :: String,

78− opt_optLevel :: Word,

7978 opt_cmdline :: [Opt], -- remember whole command line

8079 opt_origerr :: Bool,

8180 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

82− opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude

81+ opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

82+ opt_optimise :: [Optimisation]

8383 }

8484 deriving (Show, Eq)

8585

@@ -99,17 +99,22 @@ defaultOpts = IOption { opt_logLevel = 0

9999 , opt_importdirs = []

100100 , opt_triple = ""

101101 , opt_cpu = ""

102− , opt_optLevel = 2

103102 , opt_cmdline = []

104103 , opt_origerr = False

105104 , opt_autoSolve = True

106105 , opt_autoImport = []

106+ , opt_optimise = defaultOptimise

107107 }

108108

109109data PPOption = PPOption {

110110 ppopt_impl :: Bool -- ^^ whether to show implicits

111111} deriving (Show)

112112

113+data Optimisation = PETransform -- partial eval and associated transforms

114+ deriving (Show, Eq)

115+

116+defaultOptimise = [PETransform]

117+

113118-- | Pretty printing options with default verbosity.

114119defaultPPOption :: PPOption

115120defaultPPOption = PPOption { ppopt_impl = False }

@@ -416,7 +421,9 @@ data Opt = Filename String

416421 | EvalExpr String

417422 | TargetTriple String

418423 | TargetCPU String

419− | OptLevel Word

424+ | OptLevel Int

425+ | AddOpt Optimisation

426+ | RemoveOpt Optimisation

420427 | Client String

421428 | ShowOrigErr

422429 | AutoWidth -- ^ Automatically adjust terminal width

@@ -485,7 +492,7 @@ deriving instance NFData Plicity

485492impl = Imp [] Dynamic False

486493expl = Exp [] Dynamic False

487494expl_param = Exp [] Dynamic True

488−constraint = Constraint [] Dynamic

495+constraint = Constraint [] Static

489496tacimpl t = TacImp [] Dynamic t

490497

491498data FnOpt = Inlinable -- always evaluate when simplifying

src/Idris/CmdOptions.hs+3−1

@@ -80,7 +80,7 @@ parseFlags = many $

8080 <|> flag' NoBuiltins (long "nobuiltins")

8181 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

8282 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

83− <|> flag' TypeCase (long "typecase")

83+-- <|> flag' TypeCase (long "typecase")

8484 <|> flag' TypeInType (long "typeintype")

8585 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

8686 <|> flag' DefaultPartial (long "partial")

@@ -121,6 +121,8 @@ parseFlags = many $

121121 <|> flag' (OptLevel 2) (long "O2")

122122 <|> flag' (OptLevel 1) (long "O1")

123123 <|> flag' (OptLevel 0) (long "O0")

124+ <|> flag' (AddOpt PETransform) (long "partial-eval")

125+ <|> flag' (RemoveOpt PETransform) (long "no-partial-eval")

124126 <|> (OptLevel <$> option auto (short 'O' <> long "level"))

125127 <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))

126128 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

src/Idris/Elab/Class.hs+1−1

@@ -220,7 +220,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

220220

221221 insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222222 = PPi p n ty (insertConstraint c sc)

223− insertConstraint c sc = PPi (constraint) -- { pstatic = Static })

223+ insertConstraint c sc = PPi (constraint { pstatic = Static })

224224 (sMN 0 "class") c sc

225225

226226 -- make arguments explicit and don't bind class parameters

src/Idris/Elab/Clause.hs+42−25

@@ -59,6 +59,8 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

5959elabClauses info fc opts n_in cs = let n = liftname info n_in in

6060 do ctxt <- getContext

6161 ist <- getIState

62+ optimise <- getOptimise

63+ let petrans = PETransform `elem` optimise

6264 inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)

6365

6466 -- Check n actually exists, with no definition yet

@@ -74,9 +76,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

7476 let atys = map snd (getArgTys fty)

7577 cs_elab <- mapM (elabClause info opts)

7678 (zip [0..] cs)

79+ -- pats_raw is the version we'll work with at compile time:

80+ -- no simplification or PE

7781 let (pats_in, cs_full) = unzip cs_elab

78−

79− logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

82+ let pats_raw = map (simple_lhs (tt_ctxt ist)) pats_in

83+ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_raw

8084

8185 solveDeferred n

8286

@@ -94,22 +98,28 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

9498 -- If the definition is specialisable, this reduces the

9599 -- RHS

96100 pe_tm <- doPartialEval ist tpats

97− let pats = map (simple_lhs (tt_ctxt ist)) pe_tm

101+ let pats_pe = if petrans

102+ then map (simple_lhs (tt_ctxt ist)) pe_tm

103+ else pats_raw

98104

99105 let tcase = opt_typecase (idris_options ist)

100106

101107 -- Look for 'static' names and generate new specialised

102108 -- definitions for them, as well as generating rewrite rules

103109 -- for partially evaluated definitions

104− newrules <- mapM (\ e -> case e of

105− Left _ -> return []

106− Right (l, r) -> elabPE info fc n r) pats

110+ newrules <- if petrans

111+ then mapM (\ e -> case e of

112+ Left _ -> return []

113+ Right (l, r) -> elabPE info fc n r) pats_pe

114+ else return []

107115

108116 -- Redo transforms with the newly generated transformations, so

109117 -- that the specialised application we've just made gets

110118 -- used in place of the general one

111119 ist <- getIState

112− let pats_transformed = transformPats ist pats

120+ let pats_transformed = if petrans

121+ then transformPats ist pats_pe

122+ else pats_pe

113123

114124 -- Summary of what's about to happen: Definitions go:

115125 --

@@ -118,11 +128,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

118128 -- addCaseDef builds case trees from <pdef> and <pdef'>

119129

120130 -- pdef is the compile-time pattern definition.

121− -- This will get further optimised for run-time, and, separately,

122− -- further inlined to help with totality checking.

123− let pdef = map debind pats_transformed

131+ -- This will get further inlined to help with totality checking.

132+ let pdef = map debind pats_raw

133+ -- pdef_pe is the one which will get further optimised

134+ -- for run-time, and, partially evaluated

135+ let pdef_pe = map debind pats_transformed

124136

125− logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats

137+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

126138 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

127139

128140 -- NOTE: Need to store original definition so that proofs which

@@ -137,13 +149,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

137149

138150 case specNames opts of

139151 Just _ ->

140− do logLvl 2 $ "Partially evaluated:\n" ++ show pats

152+ do logLvl 2 $ "Partially evaluated:\n" ++ show pats_pe

141153 logLvl 2 $ "Transformed:\n" ++ show pats_transformed

142154 _ -> return ()

143155

144156 erInfo <- getErasureInfo <$> getIState

145157 tree@(CaseDef scargs sc _) <- tclift $

146− simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

158+ simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

147159 cov <- coverage

148160 pmissing <-

149161 if cov && not (hasDefault cs)

@@ -164,8 +176,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

164176 else return []

165177 let pcover = null pmissing

166178

167− -- pdef' is the version that gets compiled for run-time

168− pdef_in' <- applyOpts pdef

179+ -- pdef' is the version that gets compiled for run-time,

180+ -- so we start from the partially evaluated version

181+ pdef_in' <- applyOpts pdef_pe

169182 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

170183

171184 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

@@ -197,7 +210,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

197210 ctxt <- getContext

198211 ist <- getIState

199212 let opt = idris_optimisation ist

200− putIState (ist { idris_patdefs = addDef n (force pdef, force pmissing)

213+ putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

201214 (idris_patdefs ist) })

202215 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

203216 case lookupTy n ctxt of

@@ -207,8 +220,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

207220 (AssertTotal `elem` opts)

208221 atys

209222 inacc

210− pats

211− pdef pdef pdef_inl pdef' ty)

223+ pats_pe

224+ pdef

225+ pdef -- compile time

226+ pdef_inl -- inlined

227+ pdef' ty)

212228 addIBC (IBCDef n)

213229 setTotality n tot

214230 when (not reflect) $ do totcheck (fc, n)

@@ -320,7 +336,8 @@ elabPE info fc caller r =

320336 let cgns' = filter (/= n) cgns

321337 let opts = [Specialise (map (\x -> (x, Nothing)) cgns' ++

322338 (n, Just 65536) :

323− mapMaybe specName (snd specapp))]

339+ mapMaybe (specName (pe_simple specdecl))

340+ (snd specapp))]

324341 logLvl 3 $ "Specialising application: " ++ show specapp

325342 ++ " in " ++ show caller ++

326343 " with " ++ show opts

@@ -347,14 +364,14 @@ elabPE info fc caller r =

347364 -- if it doesn't work, just don't specialise. Could happen for lots

348365 -- of valid reasons (e.g. local variables in scope which can't be

349366 -- lifted out).

350− (\e -> do logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e)

367+ (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)

351368 return [])

352369

353− specName (ImplicitS, tm)

354− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

355− specName (ExplicitS, tm)

356− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

357− specName _ = Nothing

370+ specName simpl (ImplicitS, tm)

371+ | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

372+ specName simpl (ExplicitS, tm)

373+ | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

374+ specName simpl _ = Nothing

358375

359376 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

360377 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

src/Idris/PartialEval.hs+8−5

@@ -2,7 +2,7 @@

33module Idris.PartialEval(partial_eval, getSpecApps, specType,

44 mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),

5− pe_app, pe_def, pe_clauses) where

5+ pe_app, pe_def, pe_clauses, pe_simple) where

77import Idris.AbsSyntax

88import Idris.Delaborate

@@ -25,9 +25,12 @@ data PEArgType = ImplicitS -- ^ Implicit static argument

2525-- | A partially evaluated function. pe_app captures the lhs of the

2626-- new definition, pe_def captures the rhs, and pe_clauses is the

2727-- specialised implementation.

28+-- pe_simple is set if the result is always reducible, because in such a

29+-- case we'll also need to reduce the static argument

2830data PEDecl = PEDecl { pe_app :: PTerm, -- new application

2931 pe_def :: PTerm, -- old application

30− pe_clauses :: [(PTerm, PTerm)] -- clauses of new application

32+ pe_clauses :: [(PTerm, PTerm)], -- clauses of new application

33+ pe_simple :: Bool -- if just one reducible clause

3134 }

3235

3336-- | Partially evaluates given terms under the given context.

@@ -153,7 +156,7 @@ mkNewPats :: IState ->

153156-- definition isn't going to block on any of the dynamic arguments

154157-- in this case

155158mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

156− = PEDecl lhs rhs [(lhs, rhs)]

159+ = PEDecl lhs rhs [(lhs, rhs)] True

157160 where dynVar ap = case unApply ap of

158161 (_, args) -> dynArgs ns args

159162 dynArgs _ [] = True -- can definitely reduce from here

@@ -166,7 +169,7 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

166169 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

167170 dynArgs _ _ = False -- and now we'll get stuck

168171mkNewPats ist d ns newname sname lhs rhs =

169− PEDecl lhs rhs (map mkClause d)

172+ PEDecl lhs rhs (map mkClause d) False

170173 where

171174 mkClause :: (Term, Term) -> (PTerm, PTerm)

172175 mkClause (oldlhs, oldrhs)

@@ -215,7 +218,7 @@ mkPE_TermDecl ist newname sname ns

215218 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

216219 patdef = lookupCtxtExact sname (idris_patdefs ist)

217220 newpats = case patdef of

218− Nothing -> PEDecl lhs rhs [(lhs, rhs)]

221+ Nothing -> PEDecl lhs rhs [(lhs, rhs)] True

219222 Just d -> mkNewPats ist (getPats d) ns

220223 newname sname lhs rhs in

221224 newpats where

src/Idris/REPL.hs+11−2

@@ -1453,15 +1453,19 @@ idrisMain opts =

14531453 let importdirs = opt getImportDir opts

14541454 let bcs = opt getBC opts

14551455 let pkgdirs = opt getPkgDir opts

1456− let optimize = case opt getOptLevel opts of

1456+ -- Set default optimisations

1457+ let optimise = case opt getOptLevel opts of

14571458 [] -> 2

14581459 xs -> last xs

1460+ setOptLevel optimise

14591461 let outty = case opt getOutputTy opts of

14601462 [] -> Executable

14611463 xs -> last xs

14621464 let cgn = case opt getCodegen opts of

14631465 [] -> Via "c"

14641466 xs -> last xs

1467+ -- Now set/unset specifically chosen optimisations

1468+ sequence_ (opt getOptimisation opts)

14651469 script <- case opt getExecScript opts of

14661470 [] -> return Nothing

14671471 x:y:xs -> do iputStrLn "More than one interpreter expression found."

@@ -1713,10 +1717,15 @@ getCPU :: Opt -> Maybe String

17131717getCPU (TargetCPU x) = Just x

17141718getCPU _ = Nothing

17151719

1716−getOptLevel :: Opt -> Maybe Word

1720+getOptLevel :: Opt -> Maybe Int

17171721getOptLevel (OptLevel x) = Just x

17181722getOptLevel _ = Nothing

17191723

1724+getOptimisation :: Opt -> Maybe (Idris ())

1725+getOptimisation (AddOpt p) = Just $ addOptimise p

1726+getOptimisation (RemoveOpt p) = Just $ removeOptimise p

1727+getOptimisation _ = Nothing

1728+

17201729getColour :: Opt -> Maybe Bool

17211730getColour (ColourREPL b) = Just b

17221731getColour _ = Nothing

src/Idris/Transforms.hs+4−3

@@ -43,10 +43,11 @@ applyAll extra ts ap@(App f a)

4343 | (P _ fn ty, args) <- unApply ap

4444 = let rules = case lookupCtxtExact fn ts of

4545 Just r -> extra ++ r

46− Nothing -> extra in

46+ Nothing -> extra

47+ ap' = App (applyAll extra ts f) (applyAll extra ts a) in

4748 case rules of

48− [] -> App (applyAll extra ts f) (applyAll extra ts a)

49− rs -> case applyFnRules rs ap of

49+ [] -> ap'

50+ rs -> case applyFnRules rs ap' of

5051 Just tm' -> tm'

5152 _ -> App (applyAll extra ts f)

5253 (applyAll extra ts a)