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

git.iko.soy/Idris-dev

on master help sign in

Improvment on readability and usability of induction and eliminators.

1e93672Ahmad Salim Al-Sibahi13 years ago

src/Core/ProofState.hs+2−1

compare with master

unifiedsplit

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

609 mapM_ addConsHole (reverse consargs)

610 let res' = forget $ res

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

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

612− return scv

613+ return scv'

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

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

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

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

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

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

359 freshName key = do

360 nameMap <- get

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

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

362+ let name = key ++ show i

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

364− return (MN i name)

364+ return (UN name)

365

366 scrutineeName :: Name

367− scrutineeName = MN 0 "scrutinee"

367+ scrutineeName = UN "scrutinee"

368

369 scrutineeArgName :: Name

370− scrutineeArgName = MN 0 "scrutineeArg"

370+ scrutineeArgName = UN "scrutineeArg"

371

372 motiveName :: Name

373− motiveName = MN 0 "prop"

373+ motiveName = UN "prop"

374

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

376 mkMotive n paramPos params indicies =

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

460 let (_, consIdxs) = splitArgPms resTy

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

462 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))

464 where (_, idxs) = splitArgPms ty

465

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

src/Idris/Prover.hs+1−1

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

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

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

93 let OK ty = goalAtFocus ps

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

94+ let OK env = envAtFocus ps

95 iputGoal . render $

96 prettyOtherGoals hs $$

97 prettyAssumptions env $$