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

git.iko.soy/Idris-dev

on master help sign in

Some helper comments that'll be removed later

63342c7Timo Petteri Sinnemäki13 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

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

1388 PApp fc (PInferRef fc f) as'

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

1390 | 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

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

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

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

src/Idris/ElabDecls.hs+33−33

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

524 findRecArgs (ty:rs) = findRecArgs rs

525

526 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

528

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

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

531

532 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

534

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

536 getPiName (name,_,_) = name

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

548 let (_, generalIdxs') = splitArgPms resTy

549 let generalIdxs = map pexp generalIdxs'

550 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

552 let recArgs = findRecArgs consArgs

553 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

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

556 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

558 where (_, idxs) = splitArgPms recTy

559

560-- | Elaborate primitives

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

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

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

668 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

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

671 | otherwise ->

672 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

739 let ptys_u = getProjs [] cty

740 let recty = getRecTy cty

741 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

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

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

745 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

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

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

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

807 let iargs = map implicitise (zip cimp args)

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

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

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

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

810 let rhs = PRef fc (mkp pn)

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

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

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

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

825 drop (pos + 1) pls

826 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

828 [pexp (PRef fc valname),

829− pexp (PApp fc (PRef fc cn)

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

830 (map pexp lhsArgs))])

831 []

832− (PApp fc (PRef fc cn)

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

833 (map pexp rhsArgs)) []

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

835

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

873

874 mkLazy (PPi pl n ty sc)

875 = 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

877 else ty in

878 PPi pl n ty' (mkLazy sc)

879 mkLazy t = t

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

1330

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

1332propagateParams 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

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

1335 | Placeholder <- getTm t,

1336 n `elem` ps,

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

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

1340 addP _ ts = ts

1341propagateParams 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

1343propagateParams ps t x = x

1344

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

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

1492 addErrRev (crhs, clhs)

1493 return $ Right (clhs, crhs)

1494 where

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

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

1496 mkLHSapp t = t

1497

1498 decorate (NS x ns)

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

1636 mapM_ (elabDecl EAll info) wb

1637

1638 -- rhs becomes: fname' ps wval

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

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

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

1641 pexp wval :

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

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

1693 mkAux wname toplhs ns ns' c

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

1695

1696− addArg (PApp fc f args) w = PApp fc f (args ++ [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]

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

1698

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

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

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

1702 return $ substMatches mvars $

1703− PApp fc (PRef fc' wname)

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

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

1705 updateLHS n wname mvars ns ns' tm w

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

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

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

1709 | otherwise = Placeholder

1710

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

1712 fullApp x = x

1713

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

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

1727elabClass info syn doc fc constraints tn ps ds

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

1729 let tty = pibind ps PType

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

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

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

1732 -- build data declaration

1733 let mdecls = filter tydecl ds -- method declarations

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

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

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

1780 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

1782 let isConstrained = any (== t) constraints

1783 when (not isConstrained) . tclift

1784 $ 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

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

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

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

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

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

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

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

1830 let rhs = PResolveTC (fileFC "HACK")

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

1832 iLOG (showTmImpls ty)

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

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

1850 = do let ty' = insertConstraint c ty

1851 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

1853 let margs = getMArgs ty

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

1855− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs 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)

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

1857 iLOG (showTmImpls ty)

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

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

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

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

1903 [c] -> return c

1904 _ -> 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

1906 let iname = mkiname n ps expn

1907 when (what /= EDefns) $ do

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

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

1957 _ -> Nothing

1958 _ -> Nothing) ps

1959-- let lhs = PRef fc iname

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

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

1961 (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

1963 (map (pexp . mkMethApp) mtys)

1964

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

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

2042 methArgs i _ = []

2043

2044 papp fc f [] = f

2045− papp fc f as = PApp fc f as

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

2046

2047 getWParams [] = return []

2048 getWParams (p : ps)

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

2127 dc (PWith fc n t as w ds)

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

2129 (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

2131 dappname t = t

2132

2133

src/Idris/ElabTerm.hs+20−20

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

171 let fc = fileFC "Force"

172 handleError forceErr

173 (elab' ina t')

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

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

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

176 pexp ct])) True

177

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

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

223 instanceArg c)

224 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

226 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

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

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

230 pexp l, pexp r])

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

232 = do hnf_compute

233 g <- goal

234 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

236 [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

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

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

240 pexp l, pexp r])

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

247 TType _ -> asType

248 _ -> asValue

249 _ -> asType

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

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

251 [pexp t,

252 pexp (PLam n Placeholder r)])

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

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

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

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

256 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

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

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

260 pexp l, pexp r])

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

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

298 [] -> False

299 _ -> 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

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

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

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

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

369 claim valn (Var tyn)

370 letbind n (Var tyn) (Var valn)

371 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

373 env <- get_env

374 computeLet n

375 elabE (True, a, inty) sc

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

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

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

436 = 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

438 then -- simple app, as below

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

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

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

647 -- old ones with an _

648 mkClause args (l, r)

649 = 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

651 (map (mkLHSarg l) args') in

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

653

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

663 getFC d x = d

664

665 insertLazy :: PTerm -> ElabD PTerm

666− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = 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

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

668 insertLazy (PCoerced t) = return t

669 insertLazy t =

670 do ty <- goal

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

678 where

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

680 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

682

683

684 insertCoerce ina t =

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

696 return t'

697 where

698 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

700

701 -- | Elaborate the arguments to a function

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

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

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

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

719 | lazy && not pattern

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

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

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

722 pexp t])

723 | otherwise = elabArg argName holeName t

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

778pruneAlt xs = map prune xs

779 where

780 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

782 prune t = t

783

784 choose f (PAlternative a as)

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

787 case fs of

788 [a] -> a

789 _ -> 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

791 choose f t = t

792

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

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

1113 focus script

1114 ptm <- get_term

1115 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

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

1118 -- now that we have the script apply

1119 -- it to the reflected goal