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

git.iko.soy/Idris-dev

Some interactive editing fixes

Case splitting on 'case' expressions fixed, and 'with' now generated more neatly.

commit40e62938ff77216063f95912bfb4c424fd290897 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 29 Nov 2013, 16:38 (13 years ago) parenta10bcf0

8 files changed+42−18

compare with master

unifiedsplit

src/Idris/CaseSplit.hs+4−1 src/Idris/Coverage.hs+3−3 src/Idris/Delaborate.hs+15−8 src/Idris/ElabDecls.hs+6−4 src/Idris/REPL.hs+7−2 test/test032/expected+3 test/test032/input+1 test/test032/test032.idr+3

src/Idris/CaseSplit.hs+4−1

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

303303

304304 replaceRHS [] str = str

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

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

306+ replaceRHS ('=': rest) str

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

307308 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

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

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

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

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

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

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

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

6868 return new

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

7070 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

7272 | otherwise = []

7373

7474 lhsApp (PClause _ _ l _ _ _) = l

7575 lhsApp (PWith _ _ l _ _ _) = l

7676

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

7878 Right _ -> False

7979 Left miss -> True) xs

8080

src/Idris/Delaborate.hs+15−8

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

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

1515

1616delab :: 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

1821

1922delabTy :: IState -> Name -> PTerm

2023delabTy i n

2124 = case lookupTy n (tt_ctxt i) of

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

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

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

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

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

2528

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

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

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

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

2831

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

30− -> Term -> Bool -> PTerm

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

33+ -> Term

34+ -> Bool -- ^ use full names

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

36+ -> PTerm

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

3238 where

3339 un = fileFC "(val)"

3440

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

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

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

8692 (de env [] r)

87− deFn env (P _ n _) args

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

8894 = case lookup n (idris_metavars ist) of

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

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

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

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

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

93100

94101 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

728728 [] -> return ()

729729 return ()

730730 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

732732 Right _ -> False

733733 Left miss -> True) cs

734734

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

960960

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

962962 let clhs = normalise ctxt [] clhs_c

963+

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

963965

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

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

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

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

966968

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

968970 -- Elaborate where block

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

10231025 OK _ -> return ()

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

10251027 i <- getIState

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

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

10271029 return $ Right (clhs, crhs)

10281030 where

10291031 decorate (NS x ns)

src/Idris/REPL.hs+7−2

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

665665process h fn (MakeWith updatefile l n)

666666 = do src <- runIO $ readFile fn

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

668+ let ind = getIndent tyline

668669 let with = mkWith tyline n

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

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

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

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

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

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

671674 if updatefile then

672675 do let fb = fn ++ "~"

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

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

675678 unlines rest)

676679 runIO $ copyFile fb fn

677680 else ihPrintResult h with

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

682+

678683process h fn (DoProofSearch updatefile l n hints)

679684 = do src <- runIO $ readFile fn

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

test/test032/expected+3

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

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

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

1111

12+ [] => ?bar_1

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

14+

test/test032/input+1

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

33:ps 21 maprhs

44:mw 25 isElem2

55:cs 30 p

6+:cs 35 xs'

test/test032/test032.idr+3

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

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

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

3232

33+foo : List a -> List a

34+foo xs = case xs of

35+ xs' => ?bar