3729d95 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -304,6 +304,7 @@ Executable idris

304

305 , Idris.AbsSyntax

306 , Idris.AbsSyntaxTree

307+ , Idris.CaseSplit

307 , Idris.Chaser

308 , Idris.Chaser

308 , Idris.Colours

309 , Idris.Colours

309 , Idris.Completion

310 , Idris.Completion

src/Idris/AbsSyntaxTree.hs+17−4

@@ -235,6 +235,7 @@ data Command = Quit

235 | Pattelab PTerm

236 | DebugInfo Name

237 | Search PTerm

238+ | CaseSplit Name PTerm

238 | SetOpt Opt

239 | SetOpt Opt

239 | UnsetOpt Opt

240 | UnsetOpt Opt

240 | NOP

241 | NOP

@@ -1155,9 +1156,10 @@ showImp ist impl colour tm = se 10 [] tm where

1155 = let [l, r] = getExps args in

1156 = let [l, r] = getExps args in

1156 bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r

1157 bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r

1157 se p bnd (PApp _ f as)

1158 se p bnd (PApp _ f as)

1158− = let args = getExps as in

1159+ = -- let args = getExps as in

1160+ bracket p 1 $ se 1 bnd f ++

1159− bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1161+ if impl then concatMap (sArg bnd) as

1160− else concatMap (seArg bnd) args

1162+ else concatMap (suiArg impl bnd) as

1161 se p bnd (PAppBind _ f as)

1163 se p bnd (PAppBind _ f as)

1162 = let args = getExps as in

1164 = let args = getExps as in

1163 "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1165 "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

@@ -1233,8 +1235,19 @@ showImp ist impl colour tm = se 10 [] tm where

1233 sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

1235 sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

1234 sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)

1236 sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)

1235

1237

1238+ -- show argument, implicits given by the user also shown

1239+ suiArg impl bnd (PImp _ mi _ n tm _)

1240+ | impl || not mi = siArg bnd (n, tm)

1241+ suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm

1242+ suiArg impl bnd _ = ""

1243+

1236 seArg bnd arg = " " ++ se 0 bnd arg

1244 seArg bnd arg = " " ++ se 0 bnd arg

1237− siArg bnd (n, val) = " {" ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1245+ siArg bnd (n, val) =

1246+ let n' = show n

1247+ val' = se 10 bnd val in

1248+ if (n' == val')

1249+ then " {" ++ n' ++ "}"

1250+ else " {" ++ n' ++ " = " ++ val' ++ "}"

1238 scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"

1251 scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"

1239 stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1252 stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1240

1253

src/Idris/CaseSplit.hsnew file+19

@@ -0,0 +1,19 @@

1+{-# LANGUAGE PatternGuards #-}

2+

3+module Idris.CaseSplit where

4+

5+-- splitting a variable in a pattern clause

6+

7+import Idris.AbsSyntax

8+import Idris.ElabDecls

9+import Idris.ElabTerm

10+import Idris.Delaborate

11+

12+import Core.TT

13+

14+split :: Name -> PTerm -> Idris [PTerm]

15+split n t = do (tm, ty, pats) <- elabValBind toplevel True t

16+ ist <- getIState

17+ iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))

18+ iputStrLn (show pats)

19+ return [t]

src/Idris/ElabDecls.hs+15−4

@@ -730,8 +730,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

730 Nothing -> pats

731 Just ns -> partial_eval (tt_ctxt ist) ns pats

732

733+-- Elaborate a value, returning any new bindings created (this will only

734+-- happen if elaborating as a pattern clause)

735+

733−elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

736+elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

734−elabVal info aspat tm_in

737+elabValBind info aspat tm_in

735 = do ctxt <- getContext

738 = do ctxt <- getContext

736 i <- getIState

739 i <- getIState

737 let tm = addImpl i tm_in

740 let tm = addImpl i tm_in

@@ -746,15 +749,23 @@ elabVal info aspat tm_in

746-- (build i info aspat (MN 0 "val") tm))

749-- (build i info aspat (MN 0 "val") tm))

747 tclift (elaborate ctxt (MN 0 "val") infP []

750 tclift (elaborate ctxt (MN 0 "val") infP []

748 (build i info aspat (MN 0 "val") (infTerm tm)))

751 (build i info aspat (MN 0 "val") (infTerm tm)))

752+ let vtm = orderPats (getInferTerm tm')

753+ let bargs = getPBtys vtm

754+

749 def' <- checkDef (fileFC "(input)") defer

755 def' <- checkDef (fileFC "(input)") defer

750 addDeferred def'

756 addDeferred def'

751 mapM_ (elabCaseBlock info []) is

757 mapM_ (elabCaseBlock info []) is

752

758

753 logLvl 3 ("Value: " ++ show tm')

759 logLvl 3 ("Value: " ++ show tm')

754 recheckC (fileFC "(input)") [] tm'

760 recheckC (fileFC "(input)") [] tm'

755− let vtm = getInferTerm tm'

756 logLvl 2 (show vtm)

761 logLvl 2 (show vtm)

757− recheckC (fileFC "(input)") [] vtm

762+ (vtm, vty) <- recheckC (fileFC "(input)") [] vtm

763+ return (vtm, vty, bargs)

764+

765+elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

766+elabVal info aspat tm_in

767+ = do (tm, ty, _) <- elabValBind info aspat tm_in

768+ return (tm, ty)

758

769

759-- checks if the clause is a possible left hand side. Returns the term if

770-- checks if the clause is a possible left hand side. Returns the term if

760-- possible, otherwise Nothing.

771-- possible, otherwise Nothing.

src/Idris/REPL.hs+4

@@ -22,6 +22,7 @@ import Idris.Chaser

22import Idris.Imports

23import Idris.Colours

24import Idris.Inliner

25+import Idris.CaseSplit

25

26

26import Paths_idris

27import Paths_idris

27import Util.System

28import Util.System

@@ -422,6 +423,9 @@ process fn (Info n) = do i <- getIState

422 [c] -> classInfo c

423 [c] -> classInfo c

423 _ -> iPrintError "Not a class"

424 _ -> iPrintError "Not a class"

424process fn (Search t) = iPrintError "Not implemented"

425process fn (Search t) = iPrintError "Not implemented"

426+process fn (CaseSplit n t)

427+ = do tms <- split n t

428+ iputStrLn (showSep "\n" (map show tms))

425process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

429process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

426 ctxt <- getContext

430 ctxt <- getContext

427 ist <- getIState

431 ist <- getIState

src/Idris/REPLParser.hs+4

@@ -70,6 +70,10 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

70 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

71 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

72 <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

73+ <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

74+ n <- P.name;

75+ t <- P.fullExpr defaultSyntax;

76+ return (CaseSplit n t))

73 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

77 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

74 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

78 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

75 <|> do P.whiteSpace; do eof; return NOP

79 <|> do P.whiteSpace; do eof; return NOP