97319d9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Partial evaluation fixes

97319d9Edwin Brady10 years ago

src/Idris/Elab/Clause.hs+19−15

compare with master

unifiedsplit

@@ -371,8 +371,8 @@ elabPE info fc caller r =

371 mkSpecialised specapp_in = do

372 ist <- getIState

373 ctxt <- getContext

374− let (specTy, specapp) = getSpecTy ist specapp_in

374+ (specTy, specapp) <- getSpecTy ist specapp_in

375− let (n, newnm, specdecl) = getSpecClause ist specapp

375+ let (n, newnm, specdecl) = getSpecClause ist specapp specTy

376 let lhs = pe_app specdecl

377 let rhs = pe_def specdecl

378 let undef = case lookupDefExact newnm ctxt of

@@ -382,11 +382,12 @@ elabPE info fc caller r =

382 idrisCatch

383 (if (undef && all (concreteArg ist) (snd specapp)) then do

384 cgns <- getAllNames n

385+ cgns_caller <- getAllNames caller

385 -- on the RHS of the new definition, we should reduce

386 -- on the RHS of the new definition, we should reduce

386 -- everything that's not itself static (because we'll

387 -- everything that's not itself static (because we'll

387 -- want to be a PE version of those next)

388 -- want to be a PE version of those next)

388 let cgns' = filter (\x -> x /= n &&

389 let cgns' = filter (\x -> x /= n &&

389− notStatic ist x) cgns

390+ notStatic ist x) (cgns ++ cgns_caller)

390 -- set small reduction limit on partial/productive things

391 -- set small reduction limit on partial/productive things

391 let maxred = case lookupTotal n ctxt of

392 let maxred = case lookupTotal n ctxt of

392 [Total _] -> 65536

393 [Total _] -> 65536

@@ -402,18 +403,19 @@ elabPE info fc caller r =

402 (n, Just maxred) : specnames ++

403 (n, Just maxred) : specnames ++

403 concat descs)]

404 concat descs)]

404 logElab 3 $ "Specialising application: " ++ show specapp

405 logElab 3 $ "Specialising application: " ++ show specapp

405− ++ " in " ++ show caller ++

406+ ++ "\n in \n" ++ show caller ++

406− " with " ++ show opts

407+ "\n with \n" ++ show opts

408+ ++ "\nCalling: " ++ show cgns

407 logElab 3 $ "New name: " ++ show newnm

409 logElab 3 $ "New name: " ++ show newnm

408 logElab 3 $ "PE definition type : " ++ (show specTy)

410 logElab 3 $ "PE definition type : " ++ (show specTy)

409 ++ "\n" ++ show opts

411 ++ "\n" ++ show opts

410− logElab 5 $ "PE definition " ++ show newnm ++ ":\n" ++

412+ logElab 2 $ "PE definition " ++ show newnm ++ ":\n" ++

411 showSep "\n"

413 showSep "\n"

412 (map (\ (lhs, rhs) ->

414 (map (\ (lhs, rhs) ->

413 (showTmImpls lhs ++ " = " ++

415 (showTmImpls lhs ++ " = " ++

414 showTmImpls rhs)) (pe_clauses specdecl))

416 showTmImpls rhs)) (pe_clauses specdecl))

415

417

416− logElab 2 $ show n ++ " transformation rule: " ++

418+ logElab 5 $ show n ++ " transformation rule: " ++

417 showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

419 showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

418

420

419 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

421 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

@@ -429,16 +431,18 @@ elabPE info fc caller r =

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

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

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

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

431 -- lifted out).

433 -- lifted out).

432− (\e -> do logElab 3 $ "Couldn't specialise: " ++ (pshow ist e)

434+ (\e -> do logElab 5 $ "Couldn't specialise: " ++ (pshow ist e)

433 return [])

435 return [])

434

436

435 hiddenToPH (PHidden _) = Placeholder

437 hiddenToPH (PHidden _) = Placeholder

436 hiddenToPH x = x

438 hiddenToPH x = x

437

439

438− specName simpl (ImplicitS, tm)

440+ specName simpl (ImplicitS _, tm)

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

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

440 specName simpl (ExplicitS, tm)

442 specName simpl (ExplicitS, tm)

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

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

444+ specName simpl (ConstraintS, tm)

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

442 specName simpl _ = Nothing

446 specName simpl _ = Nothing

443

447

444 -- get the descendants of the name 'n' which are marked %static

448 -- get the descendants of the name 'n' which are marked %static

@@ -459,7 +463,7 @@ elabPE info fc caller r =

459 Just s -> not (or s)

463 Just s -> not (or s)

460 _ -> True

464 _ -> True

461

465

462− concreteArg ist (ImplicitS, tm) = concreteTm ist tm

466+ concreteArg ist (ImplicitS _, tm) = concreteTm ist tm

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

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

464 concreteArg ist _ = True

468 concreteArg ist _ = True

465

469

@@ -479,18 +483,18 @@ elabPE info fc caller r =

479 [ty] -> let (specty_in, args') = specType args (explicitNames ty)

483 [ty] -> let (specty_in, args') = specType args (explicitNames ty)

480 specty = normalise (tt_ctxt ist) [] (finalise specty_in)

484 specty = normalise (tt_ctxt ist) [] (finalise specty_in)

481 t = mkPE_TyDecl ist args' (explicitNames specty) in

485 t = mkPE_TyDecl ist args' (explicitNames specty) in

482− (t, (n, args'))

486+ return (t, (n, args'))

483-- (normalise (tt_ctxt ist) [] (specType args ty))

487-- (normalise (tt_ctxt ist) [] (specType args ty))

484− _ -> error "Can't happen (getSpecTy)"

488+ _ -> ifail $ "Ambiguous name " ++ show n ++ " (getSpecTy)"

485

489

486 -- get the clause of a specialised application

490 -- get the clause of a specialised application

487− getSpecClause ist (n, args)

491+ getSpecClause ist (n, args) specTy

488 = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++

492 = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++

489 qhash 5381 (showSep "_" (map showArg args))) in

493 qhash 5381 (showSep "_" (map showArg args))) in

490 -- UN (show n ++ show (map snd args)) in

494 -- UN (show n ++ show (map snd args)) in

491− (n, newnm, mkPE_TermDecl ist newnm n args)

495+ (n, newnm, mkPE_TermDecl ist newnm n specTy args)

492 where showArg (ExplicitS, n) = qshow n

496 where showArg (ExplicitS, n) = qshow n

493− showArg (ImplicitS, n) = qshow n

497+ showArg (ImplicitS _, n) = qshow n

494 showArg _ = ""

498 showArg _ = ""

495

499

496 qshow (Bind _ _ _) = "fn"

500 qshow (Bind _ _ _) = "fn"

src/Idris/Elab/Implementation.hs+2−1

@@ -192,6 +192,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

192

193 let wbVals' = map (addParams prop_params) wbVals

194

195+ logElab 5 ("Elaborating method bodies: " ++ show wbVals')

195 mapM_ (rec_elabDecl info EAll info) wbVals'

196 mapM_ (rec_elabDecl info EAll info) wbVals'

196

197

197 mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')

198 mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')

@@ -472,7 +473,7 @@ checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)

472 clookup n [] = Nothing

473 clookup n [] = Nothing

473 clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d

474 clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d

474 | otherwise = Nothing

475 | otherwise = Nothing

475−checkInjectiveDef fc ns _ = return()

476+checkInjectiveDef fc ns _ = return ()

476

477

477checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

478checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

478checkInjectiveArgs fc n ds Nothing = return ()

479checkInjectiveArgs fc n ds Nothing = return ()

src/Idris/PartialEval.hs+82−31

@@ -25,11 +25,13 @@ import Data.Maybe

25import Debug.Trace

27-- | Data type representing binding-time annotations for partial evaluation of arguments

28−data PEArgType = ImplicitS -- ^ Implicit static argument

28+data PEArgType = ImplicitS Name -- ^ Implicit static argument

29− | ImplicitD -- ^ Implicit dynamic argument

29+ | ImplicitD Name -- ^ Implicit dynamic argument

30+ | ConstraintS -- ^ Implementation constraint

31+ | ConstraintD -- ^ Implementation constraint

30− | ExplicitS -- ^ Explicit static argument

32+ | ExplicitS -- ^ Explicit static argument

31− | ExplicitD -- ^ Explicit dynamic argument

33+ | ExplicitD -- ^ Explicit dynamic argument

32− | UnifiedD -- ^ Erasable dynamic argument (found under unification)

34+ | UnifiedD -- ^ Erasable dynamic argument (found under unification)

33 deriving (Eq, Show)

35 deriving (Eq, Show)

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

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

@@ -97,7 +99,9 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

97 -- of expecting it as a function argument

99 -- of expecting it as a function argument

98 st ((ExplicitS, v) : xs) (Bind n (Pi _ t _) sc)

100 st ((ExplicitS, v) : xs) (Bind n (Pi _ t _) sc)

99 = Bind n (Let t v) (st xs sc)

101 = Bind n (Let t v) (st xs sc)

102+ st ((ImplicitS _, v) : xs) (Bind n (Pi _ t _) sc)

103+ = Bind n (Let t v) (st xs sc)

100− st ((ImplicitS, v) : xs) (Bind n (Pi _ t _) sc)

104+ st ((ConstraintS, v) : xs) (Bind n (Pi _ t _) sc)

101 = Bind n (Let t v) (st xs sc)

105 = Bind n (Let t v) (st xs sc)

102 -- Erase argument from function type

106 -- Erase argument from function type

103 st ((UnifiedD, _) : xs) (Bind n (Pi _ t _) sc)

107 st ((UnifiedD, _) : xs) (Bind n (Pi _ t _) sc)

@@ -109,7 +113,7 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

109

113

110 -- Erase implicit dynamic argument if existing argument shares it value,

114 -- Erase implicit dynamic argument if existing argument shares it value,

111 -- by substituting the value of previous argument

115 -- by substituting the value of previous argument

112− unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi i t k) sc)

116+ unifyEq (imp@(ImplicitD _, v) : xs) (Bind n (Pi i t k) sc)

113 = do amap <- get

117 = do amap <- get

114 case lookup imp amap of

118 case lookup imp amap of

115 Just n' ->

119 Just n' ->

@@ -139,11 +143,12 @@ mkPE_TyDecl ist args ty = mkty args ty

139 where

143 where

140 mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)

144 mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)

141 = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

145 = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

142− mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

146+ mkty ((ConstraintD, v) : xs) (Bind n (Pi _ t k) sc)

143 | concreteInterface ist t = mkty xs sc

147 | concreteInterface ist t = mkty xs sc

144 | interfaceConstraint ist t

148 | interfaceConstraint ist t

145 = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

149 = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

150+ mkty ((ImplicitD _, v) : xs) (Bind n (Pi _ t k) sc)

146− | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

151+ = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

147

152

148 mkty (_ : xs) t

153 mkty (_ : xs) t

149 = mkty xs t

154 = mkty xs t

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

200 (_, args) -> dynArgs ns args

205 (_, args) -> dynArgs ns args

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

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

202 -- if Static, doesn't matter what the argument is

207 -- if Static, doesn't matter what the argument is

208+ dynArgs ((ImplicitS _, _) : ns) (a : as) = dynArgs ns as

203− dynArgs ((ImplicitS, _) : ns) (a : as) = dynArgs ns as

209+ dynArgs ((ConstraintS, _) : ns) (a : as) = dynArgs ns as

204 dynArgs ((ExplicitS, _) : ns) (a : as) = dynArgs ns as

210 dynArgs ((ExplicitS, _) : ns) (a : as) = dynArgs ns as

205 -- if Dynamic, it had better be a variable or we'll need to

211 -- if Dynamic, it had better be a variable or we'll need to

206 -- do some more work

212 -- do some more work

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

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

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

210

216

211mkNewPats ist d ns newname sname lhs rhs =

217mkNewPats ist d ns newname sname lhs rhs =

212− PEDecl lhs rhs (map mkClause d) False

218+ PEDecl lhs rhs (map mkClause d) False

213 where

219 where

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

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

215 mkClause (oldlhs, oldrhs)

221 mkClause (oldlhs, oldrhs)

@@ -221,25 +227,37 @@ mkNewPats ist d ns newname sname lhs rhs =

221 (lhs, rhs)

227 (lhs, rhs)

222

228

223 mkLHSargs _ [] _ = []

229 mkLHSargs _ [] _ = []

224− -- dynamics don't appear if they're implicit

230+ -- dynamics don't appear on the LHS if they're implicit

225 mkLHSargs sub ((ExplicitD, t) : ns) (a : as)

231 mkLHSargs sub ((ExplicitD, t) : ns) (a : as)

226 = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as

232 = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as

227− mkLHSargs sub ((ImplicitD, _) : ns) (a : as)

233+ mkLHSargs sub ((ImplicitD n, t) : ns) (a : as)

234+ = pimp n (delab ist (substNames sub a)) True : mkLHSargs sub ns as

235+ mkLHSargs sub ((ConstraintD, t) : ns) (a : as)

228− = mkLHSargs sub ns as

236+ = pconst (delab ist (substNames sub a)) : mkLHSargs sub ns as

229 mkLHSargs sub ((UnifiedD, _) : ns) (a : as)

237 mkLHSargs sub ((UnifiedD, _) : ns) (a : as)

230 = mkLHSargs sub ns as

238 = mkLHSargs sub ns as

231 -- statics get dropped in any case

239 -- statics get dropped in any case

232− mkLHSargs sub ((ImplicitS, t) : ns) (a : as)

240+ mkLHSargs sub ((ImplicitS _, t) : ns) (a : as)

233 = mkLHSargs (extend a t sub) ns as

241 = mkLHSargs (extend a t sub) ns as

234 mkLHSargs sub ((ExplicitS, t) : ns) (a : as)

242 mkLHSargs sub ((ExplicitS, t) : ns) (a : as)

235 = mkLHSargs (extend a t sub) ns as

243 = mkLHSargs (extend a t sub) ns as

244+ mkLHSargs sub ((ConstraintS, t) : ns) (a : as)

245+ = mkLHSargs (extend a t sub) ns as

236 mkLHSargs sub _ [] = [] -- no more LHS

246 mkLHSargs sub _ [] = [] -- no more LHS

237

247

238 extend (P _ n _) t sub = (n, t) : sub

248 extend (P _ n _) t sub = (n, t) : sub

239 extend _ _ sub = sub

249 extend _ _ sub = sub

240

250

251+ --- 'as' are the LHS arguments

241 mkRHSargs ((ExplicitS, t) : ns) as = pexp (delab ist t) : mkRHSargs ns as

252 mkRHSargs ((ExplicitS, t) : ns) as = pexp (delab ist t) : mkRHSargs ns as

242 mkRHSargs ((ExplicitD, t) : ns) (a : as) = a : mkRHSargs ns as

253 mkRHSargs ((ExplicitD, t) : ns) (a : as) = a : mkRHSargs ns as

254+ -- Keep the implicits on the RHS, in case they got matched on

255+ mkRHSargs ((ImplicitD n, t) : ns) (a : as) = a : mkRHSargs ns as

256+ mkRHSargs ((ImplicitS n, t) : ns) as -- Dropped from LHS

257+ = pimp n (delab ist t) True : mkRHSargs ns as

258+ mkRHSargs ((ConstraintD, t) : ns) (a : as) = a : mkRHSargs ns as

259+ mkRHSargs ((ConstraintS, t) : ns) as -- Dropped from LHS

260+ = pconst (delab ist t) : mkRHSargs ns as

243 mkRHSargs (_ : ns) as = mkRHSargs ns as

261 mkRHSargs (_ : ns) as = mkRHSargs ns as

244 mkRHSargs _ _ = []

262 mkRHSargs _ _ = []

245

263

@@ -254,12 +272,26 @@ mkNewPats ist d ns newname sname lhs rhs =

254mkPE_TermDecl :: IState

272mkPE_TermDecl :: IState

255 -> Name

273 -> Name

256 -> Name

274 -> Name

275+ -> PTerm -- ^ Type of specialised function

257 -> [(PEArgType, Term)]

276 -> [(PEArgType, Term)]

258 -> PEDecl

277 -> PEDecl

259−mkPE_TermDecl ist newname sname ns

278+mkPE_TermDecl ist newname sname specty ns

279+ {- We need to erase the *dynamic* arguments

280+ where their *name* appears in the *type* of a later argument

281+ in specty.

282+ i.e. if a later dynamic argument depends on an earlier dynamic

283+ argument, we should infer the earlier one.

284+ Then we need to erase names from the LHS which no longer appear

285+ on the RHS.

286+ -}

287+ = let deps = getDepNames (eraseRet specty)

288+ lhs = eraseDeps deps $

260− = let lhs = PApp emptyFC (PRef emptyFC [] newname) (map pexp (mkp ns))

289+ PApp emptyFC (PRef emptyFC [] newname) (mkp ns)

290+ rhs = eraseDeps deps $

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

291+ delab ist (mkApp (P Ref sname Erased) (map snd ns))

292+ patdef = -- trace (showTmImpls specty ++ "\n" ++ showTmImpls lhs ++ "\n"

293+ -- ++ showTmImpls rhs) $

262− patdef = lookupCtxtExact sname (idris_patdefs ist)

294+ lookupCtxtExact sname (idris_patdefs ist)

263 newpats = case patdef of

295 newpats = case patdef of

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

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

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

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

@@ -268,17 +300,28 @@ mkPE_TermDecl ist newname sname ns

268

300

269 getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps

301 getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps

270

302

303+ eraseRet (PPi p n fc ty sc) = PPi p n fc ty (eraseRet sc)

304+ eraseRet _ = Placeholder

305+

306+ -- Get names used in later arguments; assume we've called eraseRet so there's

307+ -- no names going to appear in return type

308+ getDepNames (PPi _ n _ _ sc)

309+ | n `elem` allNamesIn sc = n : getDepNames sc

310+ | otherwise = getDepNames sc

311+ getDepNames tm = []

312+

271 mkp [] = []

313 mkp [] = []

272− mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms

314+ mkp ((ExplicitD, tm) : tms) = pexp (delab ist tm) : mkp tms

315+ mkp ((ImplicitD n, tm) : tms) = pimp n (delab ist tm) True : mkp tms

273 mkp (_ : tms) = mkp tms

316 mkp (_ : tms) = mkp tms

274

317

275− eraseImps tm = mapPT deImp tm

318+ eraseDeps ns tm = mapPT (deImp ns) tm

276

319

277− deImp (PApp fc t as) = PApp fc t (map deImpArg as)

320+ deImp ns (PApp fc t as) = PApp fc t (map (deImpArg ns) as)

278− deImp t = t

321+ deImp ns t = t

279

322

280− deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

323+ deImpArg ns a | pname a `elem` ns = a { getTm = Placeholder }

281− deImpArg a = a

324+ | otherwise = a

282

325

283-- | Get specialised applications for a given function

326-- | Get specialised applications for a given function

284getSpecApps :: IState

327getSpecApps :: IState

@@ -290,14 +333,22 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

290-- staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)

333-- staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)

291-- staticArg env True _ tm@(App f a) _ | (P _ n _, args) <- unApply tm,

334-- staticArg env True _ tm@(App f a) _ | (P _ n _, args) <- unApply tm,

292-- n `elem` env = Just (True, tm)

335-- n `elem` env = Just (True, tm)

293− staticArg env x imp tm n

336+ staticArg env True imp tm n

294− | x && imparg imp = (ImplicitS, tm)

337+ | Just n <- imparg imp = (ImplicitS n, tm)

338+ | constrarg imp = (ConstraintS, tm)

295− | x = (ExplicitS, tm)

339+ | otherwise = (ExplicitS, tm)

340+

341+ staticArg env False imp tm n

296− | imparg imp = (ImplicitD, tm)

342+ | Just nm <- imparg imp = (ImplicitD nm, (P Ref (sUN (show n ++ "arg")) Erased))

343+ | constrarg imp = (ConstraintD, tm)

297 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

344 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

298

345

299− imparg (PExp _ _ _ _) = False

346+ imparg (PExp _ _ _ _) = Nothing

300− imparg _ = True

347+ imparg (PConstraint _ _ _ _) = Nothing

348+ imparg arg = Just (pname arg)

349+

350+ constrarg (PConstraint _ _ _ _) = True

351+ constrarg arg = False

301

352

302 buildApp env [] [] _ _ = []

353 buildApp env [] [] _ _ = []

303 buildApp env (s:ss) (i:is) (a:as) (n:ns)

354 buildApp env (s:ss) (i:is) (a:as) (n:ns)

test/dsl001/expected+7−7

@@ -1,14 +1,14 @@

124

212

3testFac : Int

4−testFac = PE_interp_f79b3e31 [] (PE_fromInteger_a0377313 4)

4+testFac = PE_interp_f79b3e31 [] (PE_fromInteger_d6648df 4)

5PE_interp_f79b3e31 : Env G -> Int -> Int

6PE_interp_f79b3e31 (3arg) = \x =>

7− ifThenElse (PE_==_a03270d8 x

7+ ifThenElse (PE_==_ba2f651f x

8− (PE_fromInteger_a0377313 0))

8+ (PE_fromInteger_d6648df 0))

9− (Delay (PE_fromInteger_a0377313 1))

9+ (Delay (PE_fromInteger_d6648df 1))

10− (Delay (PE_*_a725d5d6 (PE_interp_f79b3e31 (x ::

10+ (Delay (PE_*_ba2f651f (PE_interp_f79b3e31 (x ::

11 (3arg))

12− (PE_-_a71cf640 x

12+ (PE_-_ba2f651f x

13− (PE_fromInteger_a0377313 1)))

13+ (PE_fromInteger_d6648df 1)))

14 x))

test/dsl001/test001.idr−1

@@ -101,4 +101,3 @@ main = do { printLn testFac

101 printLn test }

102

103

104−