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

git.iko.soy/Idris-dev

Add CaseSplit.hs and Command (not yet implemented)

Just the skeleton - intention is that case split on a variable and a clause will produce a list of new clauses, with dependencies expanded, when that variable is split.

commit3729d95c2911aee4d50e12337eaa7e00e1e00817 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 24 Oct 2013, 16:58 (13 years ago) parentcc780b4

6 files changed+60−8

compare with master

unifiedsplit

idris.cabal+1 src/Idris/AbsSyntaxTree.hs+17−4 src/Idris/CaseSplit.hs+19 src/Idris/ElabDecls.hs+15−4 src/Idris/REPL.hs+4 src/Idris/REPLParser.hs+4

idris.cabal+1

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

304304

305305 , Idris.AbsSyntax

306306 , Idris.AbsSyntaxTree

307+ , Idris.CaseSplit

307308 , Idris.Chaser

308309 , Idris.Colours

309310 , Idris.Completion

src/Idris/AbsSyntaxTree.hs+17−4

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

235235 | Pattelab PTerm

236236 | DebugInfo Name

237237 | Search PTerm

238+ | CaseSplit Name PTerm

238239 | SetOpt Opt

239240 | UnsetOpt Opt

240241 | NOP

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

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

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

11571158 se p bnd (PApp _ f as)

1158− = let args = getExps as in

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

1160− else concatMap (seArg bnd) args

1159+ = -- let args = getExps as in

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

1161+ if impl then concatMap (sArg bnd) as

1162+ else concatMap (suiArg impl bnd) as

11611163 se p bnd (PAppBind _ f as)

11621164 = let args = getExps as in

11631165 "!" ++ (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

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

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

12351237

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+

12361244 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' ++ "}"

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

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

12401253

src/Idris/CaseSplit.hsnew file+19

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

1+{-# LANGUAGE PatternGuards #-}

3+module Idris.CaseSplit where

5+-- splitting a variable in a pattern clause

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

730730 Nothing -> pats

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

732732

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

734−elabVal info aspat tm_in

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

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

735+

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

737+elabValBind info aspat tm_in

735738 = do ctxt <- getContext

736739 i <- getIState

737740 let tm = addImpl i tm_in

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

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

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

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

752+ let vtm = orderPats (getInferTerm tm')

753+ let bargs = getPBtys vtm

754+

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

750756 addDeferred def'

751757 mapM_ (elabCaseBlock info []) is

752758

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

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

755− let vtm = getInferTerm tm'

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

758769

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

760771-- possible, otherwise Nothing.

src/Idris/REPL.hs+4

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

2222import Idris.Imports

2323import Idris.Colours

2424import Idris.Inliner

25+import Idris.CaseSplit

2526

2627import Paths_idris

2728import Util.System

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

422423 [c] -> classInfo c

423424 _ -> iPrintError "Not a class"

424425process 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))

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

426430 ctxt <- getContext

427431 ist <- getIState

src/Idris/REPLParser.hs+4

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

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

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

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

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

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

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