40e6293 · Idris-dev · git.iko.soy

src/Idris/CaseSplit.hs+4−1

compare with master

unifiedsplit

@@ -303,5 +303,8 @@ mkWith str n = let ind = getIndent str

303

304 replaceRHS [] str = str

305 replaceRHS ('?':'=': rest) str = str

306− replaceRHS ('=': rest) str = str

306+ replaceRHS ('=': rest) str

307+ | not ('=' `elem` rest) = str

307 replaceRHS (x : rest) str = x : replaceRHS rest str

308 replaceRHS (x : rest) str = x : replaceRHS rest str

309+

310+

src/Idris/Coverage.hs+3−3

@@ -50,7 +50,7 @@ genClauses fc n xs given

50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

51 logLvl 10 $ show argss ++ "\n" ++ show all_args

52 logLvl 10 $ "Original: \n" ++

53− showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True)) xs)

53+ showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)

54 -- add an infinite supply of explicit arguments to update the possible

55 -- cases for (the return type may be variadic, or function type, sp

56 -- there may be more case splitting that the idris_implicits record

@@ -68,13 +68,13 @@ genClauses fc n xs given

68 return new

69-- return (map (\t -> PClause n t [] PImpossible []) new)

70 where getLHS i term

71− | (f, args) <- unApply term = map (\t -> delab' i t True) args

71+ | (f, args) <- unApply term = map (\t -> delab' i t True True) args

72 | otherwise = []

73

74 lhsApp (PClause _ _ l _ _ _) = l

75 lhsApp (PWith _ _ l _ _ _) = l

76

77− noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of

77+ noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of

78 Right _ -> False

79 Left miss -> True) xs

80

src/Idris/Delaborate.hs+15−8

@@ -14,21 +14,27 @@ import Debug.Trace

14bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

15

16delab :: IState -> Term -> PTerm

17−delab i tm = delab' i tm False

17+delab i tm = delab' i tm False False

18+

19+delabMV :: IState -> Term -> PTerm

20+delabMV i tm = delab' i tm False True

18

21

19delabTy :: IState -> Name -> PTerm

22delabTy :: IState -> Name -> PTerm

20delabTy i n

23delabTy i n

21 = case lookupTy n (tt_ctxt i) of

24 = case lookupTy n (tt_ctxt i) of

22 (ty:_) -> case lookupCtxt n (idris_implicits i) of

25 (ty:_) -> case lookupCtxt n (idris_implicits i) of

23− (imps:_) -> delabTy' i imps ty False

26+ (imps:_) -> delabTy' i imps ty False False

24− _ -> delabTy' i [] ty False

27+ _ -> delabTy' i [] ty False False

25

28

26−delab' :: IState -> Term -> Bool -> PTerm

29+delab' :: IState -> Term -> Bool -> Bool -> PTerm

27−delab' i t f = delabTy' i [] t f

30+delab' i t f mvs = delabTy' i [] t f mvs

28

31

29delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

32delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

33+ -> Term

34+ -> Bool -- ^ use full names

35+ -> Bool -- ^ Don't treat metavariables specially

30− -> Term -> Bool -> PTerm

36+ -> PTerm

31−delabTy' ist imps tm fullname = de [] imps tm

37+delabTy' ist imps tm fullname mvs = de [] imps tm

32 where

38 where

33 un = fileFC "(val)"

39 un = fileFC "(val)"

34

40

@@ -84,11 +90,12 @@ delabTy' ist imps tm fullname = de [] imps tm

84 | n == eqTy = PEq un (de env [] l) (de env [] r)

90 | n == eqTy = PEq un (de env [] l) (de env [] r)

85 | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder

91 | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder

86 (de env [] r)

92 (de env [] r)

87− deFn env (P _ n _) args

93+ deFn env (P _ n _) args | not mvs

88 = case lookup n (idris_metavars ist) of

94 = case lookup n (idris_metavars ist) of

89 Just (Just _, mi, _) ->

95 Just (Just _, mi, _) ->

90 mkMVApp (dens n) (drop mi (map (de env []) args))

96 mkMVApp (dens n) (drop mi (map (de env []) args))

91 _ -> mkPApp (dens n) (map (de env []) args)

97 _ -> mkPApp (dens n) (map (de env []) args)

98+ | otherwise = mkPApp (dens n) (map (de env []) args)

92 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

99 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

93

100

94 mkMVApp n []

101 mkMVApp n []

src/Idris/ElabDecls.hs+6−4

@@ -728,7 +728,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

728 [] -> return ()

729 return ()

730 where

731− noMatch i cs tm = all (\x -> case matchClause i (delab' i x True) tm of

731+ noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of

732 Right _ -> False

733 Left miss -> True) cs

734

@@ -960,9 +960,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

960

961 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

962 let clhs = normalise ctxt [] clhs_c

963+

964+ logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

963

965

964− addInternalApp (fc_fname fc) (fc_line fc) (delab i clhs)

966+ addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

965− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i clhs))

967+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

966

968

967 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

969 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

968 -- Elaborate where block

970 -- Elaborate where block

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

1023 OK _ -> return ()

1025 OK _ -> return ()

1024 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

1026 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

1025 i <- getIState

1027 i <- getIState

1026− checkInferred fc (delab' i crhs True) rhs

1028+ checkInferred fc (delab' i crhs True True) rhs

1027 return $ Right (clhs, crhs)

1029 return $ Right (clhs, crhs)

1028 where

1030 where

1029 decorate (NS x ns)

1031 decorate (NS x ns)

src/Idris/REPL.hs+7−2

@@ -665,9 +665,12 @@ process h fn (AddMissing updatefile l n)

665process h fn (MakeWith updatefile l n)

666 = do src <- runIO $ readFile fn

667 let (before, tyline : later) = splitAt (l-1) (lines src)

668+ let ind = getIndent tyline

668 let with = mkWith tyline n

669 let with = mkWith tyline n

669− -- add clause before first blank line in 'later'

670+ -- add clause before first blank line in 'later',

671+ -- or (TODO) before first line with same indentation as tyline

670− let (nonblank, rest) = span (not . all isSpace) later

672+ let (nonblank, rest) = span (\x -> not (all isSpace x) &&

673+ not (ind == getIndent x)) later

671 if updatefile then

674 if updatefile then

672 do let fb = fn ++ "~"

675 do let fb = fn ++ "~"

673 runIO $ writeFile fb (unlines (before ++ nonblank)

676 runIO $ writeFile fb (unlines (before ++ nonblank)

@@ -675,6 +678,8 @@ process h fn (MakeWith updatefile l n)

675 unlines rest)

678 unlines rest)

676 runIO $ copyFile fb fn

679 runIO $ copyFile fb fn

677 else ihPrintResult h with

680 else ihPrintResult h with

681+ where getIndent s = length (takeWhile isSpace s)

682+

678process h fn (DoProofSearch updatefile l n hints)

683process h fn (DoProofSearch updatefile l n hints)

679 = do src <- runIO $ readFile fn

684 = do src <- runIO $ readFile fn

680 let (before, tyline : later) = splitAt (l-1) (lines src)

685 let (before, tyline : later) = splitAt (l-1) (lines src)

test/test032/expected+3

@@ -9,3 +9,6 @@ isElem2 x (y :: ys) with (_)

9 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3

11

12+ [] => ?bar_1

13+ (_ :: _) => ?bar_2

14+

test/test032/input+1

@@ -3,3 +3,4 @@

3:ps 21 maprhs

4:mw 25 isElem2

5:cs 30 p

6+:cs 35 xs'

test/test032/test032.idr+3

@@ -30,3 +30,6 @@ isElem3 x (y :: ys) with (decEq x y)

30 isElem3 x (y :: ys) | (Yes p) = ?isElem3_rhs_1

31 isElem3 x (y :: ys) | (No _) = ?isElem3_rhs_2

32

33+foo : List a -> List a

34+foo xs = case xs of

35+ xs' => ?bar