63342c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some helper comments that'll be removed later

commit63342c7f2d4e9a817771fb468198f5dfabf189d1 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateFri 28 Mar 2014, 11:58 (13 years ago) parentb2b5545

3 files changed+54−54

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabDecls.hs+33−33 src/Idris/ElabTerm.hs+20−20

src/Idris/AbsSyntax.hs+1−1

@@ -1388,7 +1388,7 @@ addImpl' inpat env infns ist ptm

13881388 PApp fc (PInferRef fc f) as'

13891389 ai env ds (PApp fc ftm@(PRef _ f) as)

13901390 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)

1391− | not (f `elem` map fst env)

1391+ | not (f `elem` map fst env) -- notelocal

13921392 = let as' = map (fmap (ai env ds)) as in

13931393 handleErr $ aiFn inpat False ist fc f ds as'

13941394 | Just (Just ty) <- lookup f env =

src/Idris/ElabDecls.hs+33−33

@@ -524,13 +524,13 @@ elabEliminator paramPos n ty cons info = do

524524 findRecArgs (ty:rs) = findRecArgs rs

525525

526526 applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm

527− applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)

527+ applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs) -- ipapp

528528

529529 convertArg :: (Name, Plicity, PTerm) -> PArg

530530 convertArg (n, _, _) = pexp (PRef elimFC n)

531531

532532 applyMotive :: [PTerm] -> PTerm -> PTerm

533− applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])

533+ applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t]) -- ipapp

534534

535535 getPiName :: (Name, Plicity, PTerm) -> Name

536536 getPiName (name,_,_) = name

@@ -548,13 +548,13 @@ elabEliminator paramPos n ty cons info = do

548548 let (_, generalIdxs') = splitArgPms resTy

549549 let generalIdxs = map pexp generalIdxs'

550550 consArgs <- namePis True args

551− let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

551+ let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs]) -- ipapp

552552 let recArgs = findRecArgs consArgs

553553 let recElims = map applyRecElim recArgs

554− let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

554+ let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims) -- ipapp

555555 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

556556 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

557− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])

557+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm]) -- ipapp

558558 where (_, idxs) = splitArgPms recTy

559559

560560-- | Elaborate primitives

@@ -666,7 +666,7 @@ elabProvider info syn fc what n ty tm

666666 | what `elem` [ProvTerm, ProvAny] ->

667667 do -- Finally add a top-level definition of the provided term

668668 elabType info syn "" [] fc [] n ty

669− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

669+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []] -- ipapp

670670 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

671671 | otherwise ->

672672 ierror . Msg $ "Attempted to provide a term where a postulate was expected."

@@ -739,7 +739,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

739739 let ptys_u = getProjs [] cty

740740 let recty = getRecTy cty

741741 logLvl 6 $ show (recty, ptys)

742− let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)

742+ let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n) -- ipapp

743743 [pexp (PRef fc rec)])) ptys

744744 proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])

745745 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

@@ -805,8 +805,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

805805 let after = length substs - (pos + 1)

806806 let args = take before pls ++ PRef fc (mkp pn) : take after pls

807807 let iargs = map implicitise (zip cimp args)

808− let lhs = PApp fc (PRef fc pn)

809− [pexp (PApp fc (PRef fc cn) iargs)]

808+ let lhs = PApp fc (PRef fc pn) -- ipapp

809+ [pexp (PApp fc (PRef fc cn) iargs)] -- ipapp

810810 let rhs = PRef fc (mkp pn)

811811 let pclause = PClause fc pn lhs [] rhs []

812812 return [pfnTy, PClauses fc [] pn [pclause]]

@@ -824,12 +824,12 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

824824 let rhsArgs = take pos pls ++ (PRef fc valname) :

825825 drop (pos + 1) pls

826826 let before = pos

827− let pclause = PClause fc setname (PApp fc (PRef fc setname)

827+ let pclause = PClause fc setname (PApp fc (PRef fc setname) -- ipapp

828828 [pexp (PRef fc valname),

829− pexp (PApp fc (PRef fc cn)

829+ pexp (PApp fc (PRef fc cn) -- ipapp

830830 (map pexp lhsArgs))])

831831 []

832− (PApp fc (PRef fc cn)

832+ (PApp fc (PRef fc cn) -- ipapp

833833 (map pexp rhsArgs)) []

834834 return (pn, pfnTy, PClauses fc [] setname [pclause])

835835

@@ -873,7 +873,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

873873

874874 mkLazy (PPi pl n ty sc)

875875 = let ty' = if getTyName ty

876− then PApp fc (PRef fc (sUN "Lazy")) [pexp ty]

876+ then PApp fc (PRef fc (sUN "Lazy")) [pexp ty] -- ipapp

877877 else ty in

878878 PPi pl n ty' (mkLazy sc)

879879 mkLazy t = t

@@ -1330,7 +1330,7 @@ paramNames args env (p : ps)

13301330

13311331propagateParams :: [Name] -> Type -> PTerm -> PTerm

13321332propagateParams ps t tm@(PApp _ (PRef fc n) args)

1333− = PApp fc (PRef fc n) (addP t args)

1333+ = PApp fc (PRef fc n) (addP t args) -- tpapp

13341334 where addP (Bind n _ sc) (t : ts)

13351335 | Placeholder <- getTm t,

13361336 n `elem` ps,

@@ -1339,7 +1339,7 @@ propagateParams ps t tm@(PApp _ (PRef fc n) args)

13391339 addP (Bind n _ sc) (t : ts) = t : addP sc ts

13401340 addP _ ts = ts

13411341propagateParams ps t (PRef fc n)

1342− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1342+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps) -- ipapp

13431343propagateParams ps t x = x

13441344

13451345elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

@@ -1492,7 +1492,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

14921492 addErrRev (crhs, clhs)

14931493 return $ Right (clhs, crhs)

14941494 where

1495− mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

1495+ mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t [] -- ipapp

14961496 mkLHSapp t = t

14971497

14981498 decorate (NS x ns)

@@ -1636,7 +1636,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

16361636 mapM_ (elabDecl EAll info) wb

16371637

16381638 -- rhs becomes: fname' ps wval

1639− let rhs = PApp fc (PRef fc wname)

1639+ let rhs = PApp fc (PRef fc wname) -- ipapp

16401640 (map (pexp . (PRef fc) . fst) bargs_pre ++

16411641 pexp wval :

16421642 (map (pexp . (PRef fc) . fst) bargs_post))

@@ -1693,14 +1693,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

16931693 mkAux wname toplhs ns ns' c

16941694 = ifail $ show fc ++ "badly formed with clause"

16951695

1696− addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

1697− addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

1696+ addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w]) -- tpapp

1697+ addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w] -- ipapp

16981698

16991699 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

17001700 = let ns = map (keepMvar (map fst mvars) fc') ns_in

17011701 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

17021702 return $ substMatches mvars $

1703− PApp fc (PRef fc' wname)

1703+ PApp fc (PRef fc' wname) -- tpapp

17041704 (map pexp ns ++ pexp w : (map pexp ns'))

17051705 updateLHS n wname mvars ns ns' tm w

17061706 = ifail $ "Not implemented match " ++ show tm

@@ -1708,7 +1708,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

17081708 keepMvar mvs fc v | v `elem` mvs = PRef fc v

17091709 | otherwise = Placeholder

17101710

1711− fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1711+ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs)) -- tpapp

17121712 fullApp x = x

17131713

17141714 split [] rest pre = (reverse pre, rest)

@@ -1727,7 +1727,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

17271727elabClass info syn doc fc constraints tn ps ds

17281728 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

17291729 let tty = pibind ps PType

1730− let constraint = PApp fc (PRef fc tn)

1730+ let constraint = PApp fc (PRef fc tn) -- ipapp

17311731 (map (pexp . PRef fc) (map fst ps))

17321732 -- build data declaration

17331733 let mdecls = filter tydecl ds -- method declarations

@@ -1778,7 +1778,7 @@ elabClass info syn doc fc constraints tn ps ds

17781778 = do when (not $ null cs) . tclift

17791779 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

17801780 i <- getIState

1781− let t = PApp fc (PRef fc n) (map pexp ps)

1781+ let t = PApp fc (PRef fc n) (map pexp ps) -- ipapp

17821782 let isConstrained = any (== t) constraints

17831783 when (not isConstrained) . tclift

17841784 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

@@ -1825,8 +1825,8 @@ elabClass info syn doc fc constraints tn ps ds

18251825 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

18261826 -- SN (ParentN cn (show con))

18271827 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

1828− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1829− let lhs = PApp fc (PRef fc cfn) [pconst capp]

1828+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) -- ipapp

1829+ let lhs = PApp fc (PRef fc cfn) [pconst capp] -- ipapp

18301830 let rhs = PResolveTC (fileFC "HACK")

18311831 let ty = PPi constraint (sMN 0 "pc") c con

18321832 iLOG (showTmImpls ty)

@@ -1849,11 +1849,11 @@ elabClass info syn doc fc constraints tn ps ds

18491849 tfun cn c syn all (m, (doc, o, ty))

18501850 = do let ty' = insertConstraint c ty

18511851 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

1852− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1852+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) -- ipapp

18531853 let margs = getMArgs ty

18541854 let anames = map (\x -> sMN x "arg") [0..]

1855− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1856− let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1855+ let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames) -- ipapp

1856+ let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames) -- ipapp

18571857 iLOG (showTmImpls ty)

18581858 iLOG (show (m, ty', capp, margs))

18591859 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

@@ -1902,7 +1902,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

19021902 (n, ci) <- case lookupCtxtName n (idris_classes i) of

19031903 [c] -> return c

19041904 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

1905− let constraint = PApp fc (PRef fc n) (map pexp ps)

1905+ let constraint = PApp fc (PRef fc n) (map pexp ps) -- ipapp

19061906 let iname = mkiname n ps expn

19071907 when (what /= EDefns) $ do

19081908 nty <- elabType' True info syn "" [] fc [] iname t

@@ -1957,9 +1957,9 @@ elabInstance info syn what fc cs n ps t expn ds = do

19571957 _ -> Nothing

19581958 _ -> Nothing) ps

19591959-- let lhs = PRef fc iname

1960− let lhs = PApp fc (PRef fc iname)

1960+ let lhs = PApp fc (PRef fc iname) -- ipapp

19611961 (map (\n -> pimp n (PRef fc n) True) headVars)

1962− let rhs = PApp fc (PRef fc (instanceName ci))

1962+ let rhs = PApp fc (PRef fc (instanceName ci)) -- ipapp

19631963 (map (pexp . mkMethApp) mtys)

19641964

19651965 logLvl 5 $ "Instance LHS " ++ show lhs

@@ -2042,7 +2042,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20422042 methArgs i _ = []

20432043

20442044 papp fc f [] = f

2045− papp fc f as = PApp fc f as

2045+ papp fc f as = PApp fc f as -- ipapp

20462046

20472047 getWParams [] = return []

20482048 getWParams (p : ps)

@@ -2127,7 +2127,7 @@ decorateid decorate (PClauses f o n cs)

21272127 dc (PWith fc n t as w ds)

21282128 = PWith fc (decorate n) (dappname t) as w

21292129 (map (decorateid decorate) ds)

2130− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

2130+ dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as -- tpapp

21312131 dappname t = t

21322132

21332133

src/Idris/ElabTerm.hs+20−20

@@ -171,7 +171,7 @@ elab ist info pattern opts fn tm

171171 let fc = fileFC "Force"

172172 handleError forceErr

173173 (elab' ina t')

174− (elab' ina (PApp fc (PRef fc (sUN "Force"))

174+ (elab' ina (PApp fc (PRef fc (sUN "Force")) -- ipapp

175175 [pimp (sUN "a") Placeholder True,

176176 pexp ct])) True

177177

@@ -222,9 +222,9 @@ elab ist info pattern opts fn tm

222222 (do c <- getNameFrom (sMN 0 "class")

223223 instanceArg c)

224224 elab' ina (PRefl fc t)

225− = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

225+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True, -- ipapp

226226 pimp (sMN 0 "x") t False])

227− elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

227+ elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) -- ipapp

228228 [pimp (sMN 0 "A") Placeholder True,

229229 pimp (sMN 0 "B") Placeholder False,

230230 pexp l, pexp r])

@@ -232,9 +232,9 @@ elab ist info pattern opts fn tm

232232 = do hnf_compute

233233 g <- goal

234234 case g of

235− TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)

235+ TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy) -- ipapp

236236 [pexp l,pexp r])

237− _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)

237+ _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon) -- ipapp

238238 [pimp (sMN 0 "A") Placeholder True,

239239 pimp (sMN 0 "B") Placeholder True,

240240 pexp l, pexp r])

@@ -247,14 +247,14 @@ elab ist info pattern opts fn tm

247247 TType _ -> asType

248248 _ -> asValue

249249 _ -> asType

250− where asType = elab' ina (PApp fc (PRef fc sigmaTy)

250+ where asType = elab' ina (PApp fc (PRef fc sigmaTy) -- ipapp

251251 [pexp t,

252252 pexp (PLam n Placeholder r)])

253− asValue = elab' ina (PApp fc (PRef fc existsCon)

253+ asValue = elab' ina (PApp fc (PRef fc existsCon) -- ipapp

254254 [pimp (sMN 0 "a") t False,

255255 pimp (sMN 0 "P") Placeholder True,

256256 pexp l, pexp r])

257− elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)

257+ elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon) -- ipapp

258258 [pimp (sMN 0 "a") t False,

259259 pimp (sMN 0 "P") Placeholder True,

260260 pexp l, pexp r])

@@ -297,7 +297,7 @@ elab ist info pattern opts fn tm

297297 where inparamBlock n = case lookupCtxtName n (inblock info) of

298298 [] -> False

299299 _ -> True

300− elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

300+ elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f []) -- ipapp

301301 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

302302 elab' ina@(_, a, inty) (PLam n Placeholder sc)

303303 = do -- if n is a type constructor name, this makes no sense...

@@ -369,7 +369,7 @@ elab ist info pattern opts fn tm

369369 claim valn (Var tyn)

370370 letbind n (Var tyn) (Var valn)

371371 focus valn

372− elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])

372+ elabE (True, a, True) (PApp fc r [pexp (delab ist rty)]) -- ipapp

373373 env <- get_env

374374 computeLet n

375375 elabE (True, a, inty) sc

@@ -434,7 +434,7 @@ elab ist info pattern opts fn tm

434434 -- if f is local, just do a simple_app

435435 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

436436 = do env <- get_env

437− if (f `elem` map fst env && length args == 1)

437+ if (f `elem` map fst env && length args == 1) -- notelocal

438438 then -- simple app, as below

439439 do simple_app (elabE (ina, g, inty) (PRef fc f))

440440 (elabE (True, g, inty) (getTm (head args)))

@@ -647,7 +647,7 @@ elab ist info pattern opts fn tm

647647 -- old ones with an _

648648 mkClause args (l, r)

649649 = let args' = map (shadowed (allNamesIn l)) args

650− lhs = PApp (getFC fc l) (PRef (getFC fc l) n)

650+ lhs = PApp (getFC fc l) (PRef (getFC fc l) n) -- ipapp

651651 (map (mkLHSarg l) args') in

652652 PClause (getFC fc l) n lhs [] r []

653653

@@ -663,8 +663,8 @@ elab ist info pattern opts fn tm

663663 getFC d x = d

664664

665665 insertLazy :: PTerm -> ElabD PTerm

666− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

667− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t

666+ insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t -- tpapp

667+ insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t -- tpapp

668668 insertLazy (PCoerced t) = return t

669669 insertLazy t =

670670 do ty <- goal

@@ -678,7 +678,7 @@ elab ist info pattern opts fn tm

678678 where

679679 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

680680 mkDelay t = let fc = fileFC "Delay" in

681− addImpl ist (PApp fc (PRef fc (sUN "Delay")) [pexp t])

681+ addImpl ist (PApp fc (PRef fc (sUN "Delay")) [pexp t]) -- ipapp

682682

683683

684684 insertCoerce ina t =

@@ -696,7 +696,7 @@ elab ist info pattern opts fn tm

696696 return t'

697697 where

698698 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

699− addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

699+ addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)]) -- ipapp

700700

701701 -- | Elaborate the arguments to a function

702702 elabArgs :: IState -- ^ The current Idris state

@@ -717,7 +717,7 @@ elab ist info pattern opts fn tm

717717 = elabArgs ist ina failed fc r f ns force args

718718 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

719719 | lazy && not pattern

720− = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

720+ = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy")) -- ipapp

721721 [pimp (sUN "a") Placeholder True,

722722 pexp t])

723723 | otherwise = elabArg argName holeName t

@@ -778,7 +778,7 @@ pruneAlt :: [PTerm] -> [PTerm]

778778pruneAlt xs = map prune xs

779779 where

780780 prune (PApp fc1 (PRef fc2 f) as)

781− = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

781+ = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as) -- tpapp

782782 prune t = t

783783

784784 choose f (PAlternative a as)

@@ -787,7 +787,7 @@ pruneAlt xs = map prune xs

787787 case fs of

788788 [a] -> a

789789 _ -> PAlternative a as'

790− choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

790+ choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as) -- tpapp

791791 choose f t = t

792792

793793 headIs f (PApp _ (PRef _ f') _) = f == f'

@@ -1113,7 +1113,7 @@ runTac autoSolve ist fn tac

11131113 focus script

11141114 ptm <- get_term

11151115 elab ist toplevel False [] (sMN 0 "tac")

1116− (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

1116+ (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)]) -- ipapp

11171117 (script', _) <- get_type_val (Var scriptvar)

11181118 -- now that we have the script apply

11191119 -- it to the reflected goal