1e93672 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improvment on readability and usability of induction and eliminators.

commit1e9367264384a4ee9fc02c0af656fd37685e772b authorAhmad Salim Al-Sibahi <asal@itu.dk> dateTue 10 Dec 2013, 13:03 (13 years ago) parent2dc07fa

3 files changed+9−8

compare with master

unifiedsplit

src/Core/ProofState.hs+2−1 src/Idris/ElabDecls.hs+6−6 src/Idris/Prover.hs+1−1

src/Core/ProofState.hs+2−1

@@ -609,7 +609,8 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

609609 mapM_ addConsHole (reverse consargs)

610610 let res' = forget $ res

611611 (scv, sct) <- lift $ check ctxt env res'

612− return scv

612+ let scv' = specialise ctxt env [] scv

613+ return scv'

613614 [] -> fail $ "Induction needs an eliminator for " ++ show nm

614615 xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show nm

615616 (P _ nm _, _) -> fail "Induction not yet supported for types with arguments"

src/Idris/ElabDecls.hs+6−6

@@ -359,18 +359,18 @@ elabEliminator paramPos n ty cons info = do

359359 freshName key = do

360360 nameMap <- get

361361 let i = fromMaybe 0 (Map.lookup key nameMap)

362− let name = key ++ show i ++ "__"

362+ let name = key ++ show i

363363 put $ Map.insert key (i+1) nameMap

364− return (MN i name)

364+ return (UN name)

365365

366366 scrutineeName :: Name

367− scrutineeName = MN 0 "scrutinee"

367+ scrutineeName = UN "scrutinee"

368368

369369 scrutineeArgName :: Name

370− scrutineeArgName = MN 0 "scrutineeArg"

370+ scrutineeArgName = UN "scrutineeArg"

371371

372372 motiveName :: Name

373− motiveName = MN 0 "prop"

373+ motiveName = UN "prop"

374374

375375 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

376376 mkMotive n paramPos params indicies =

@@ -460,7 +460,7 @@ elabEliminator paramPos n ty cons info = do

460460 let (_, consIdxs) = splitArgPms resTy

461461 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

462462 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

463− applyRecMotive (n,_,ty) = (MN 0 $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

463+ applyRecMotive (n,_,ty) = (UN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

464464 where (_, idxs) = splitArgPms ty

465465

466466 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

src/Idris/Prover.hs+1−1

@@ -91,7 +91,7 @@ dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

9191 iputGoal . render $ pretty nm <> colon <+> text "No more goals."

9292dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

9393 let OK ty = goalAtFocus ps

94− let OK env = trace (show $ envAtFocus ps) $ envAtFocus ps

94+ let OK env = envAtFocus ps

9595 iputGoal . render $

9696 prettyOtherGoals hs $$

9797 prettyAssumptions env $$