46256ab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add ':addclause' command at the REPL

:addclause l n will find the name 'n' on line 'l', which should be a type declaration, and print a corresponding clause for it. :addclause! does the same, but adds it to the first blank line after that in the file vim script updated so that 'cd' does the corresponding thing (moving back to find the type declaration before the cursor)

commit46256ab939e3ddea164f5289f993580b12ac2560 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 28 Oct 2013, 10:47 (13 years ago) parent328dfe6

9 files changed+150−47

compare with master

unifiedsplit

contribs/idriscasesplit.vim+52−8 src/Idris/AbsSyntax.hs+6−6 src/Idris/AbsSyntaxTree.hs+15−9 src/Idris/CaseSplit.hs+18−1 src/Idris/ElabDecls.hs+17−11 src/Idris/IBC.hs+9−5 src/Idris/ParseExpr.hs+3−3 src/Idris/REPL.hs+23−1 src/Idris/REPLParser.hs+7−3

contribs/idriscasesplit.vim+52−8

@@ -1,21 +1,65 @@

1+function IdrisReload()

2+ let tc = system("idris --client :r")

3+ if (! (tc is ""))

4+ echo tc

5+ endif

6+ return tc

7+endfunction

9+function IdrisShowType()

10+ let word = expand("<cword>")

11+ let tc = IdrisReload()

12+ if (! (tc is ""))

13+ echo tc

14+ else

15+ let ty = system("idris --client :t " . word)

16+ echo ty

17+ endif

18+ return tc

19+endfunction

120

2−function CaseSplit()

21+function IdrisCaseSplit()

322 let view = winsaveview()

423 w

524 let cline = line(".")

625 let word = expand("<cword>")

7− let fn = "idris --client :cs! " . cline . " " . word

8− let tc = system("idris --client :r")

26+ let tc = IdrisReload()

27+

928 if (tc is "")

29+ let fn = "idris --client :cs! " . cline . " " . word

1030 let result = system(fn)

11− e

12− call winrestview(view)

1331 if (! (result is ""))

1432 echo result

33+ else

34+ e

35+ call winrestview(view)

1536 endif

16− else

17− echo tc

1837 endif

1938endfunction

2039

21−map ci :call CaseSplit()<ENTER>

40+function IdrisAddClause()

41+ let view = winsaveview()

42+ w

43+ let cline = line(".")

44+ let word = expand("<cword>")

45+ let tc = IdrisReload()

46+

47+ if (tc is "")

48+ let fn = "idris --client :ac! " . cline . " " . word

49+ let result = system(fn)

50+ if (! (result is ""))

51+ echo result

52+ else

53+ e

54+ call winrestview(view)

55+ call search(word)

56+

57+ endif

58+ endif

59+endfunction

60+

61+map ct :call IdrisShowType()<ENTER>

62+map cr :call IdrisReload()<ENTER>

63+map ci :call IdrisCaseSplit()<ENTER>

64+map cd ?:<ENTER>b:call IdrisAddClause()<ENTER>w

65+

src/Idris/AbsSyntax.hs+6−6

@@ -668,7 +668,7 @@ piBind = piBindp expl

668668

669669piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

670670piBindp p [] t = t

671−piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)

671+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

672672

673673-- Dealing with parameters

674674

@@ -761,7 +761,7 @@ expandParamsD :: Bool -> -- True = RHS only

761761expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)

762762 = if n `elem` ns && (not rhsonly)

763763 then -- trace (show (n, expandParams dec ps ns ty)) $

764− PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))

764+ PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

765765 else --trace (show (n, expandParams dec ps ns ty)) $

766766 PTy doc syn fc o n (expandParams dec ps ns [] ty)

767767expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

@@ -989,13 +989,13 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

989989 = do (decls, ns) <- get

990990 let isn = concatMap (namesIn uvars ist) (map getTm as)

991991 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

992− imps top env (PPi (Imp l _ doc) n ty sc)

992+ imps top env (PPi (Imp l _ doc _) n ty sc)

993993 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

994994 (decls , ns) <- get

995995 put (PImp (getPriority ist ty) True l n ty doc : decls,

996996 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

997997 imps True (n:env) sc

998− imps top env (PPi (Exp l _ doc) n ty sc)

998+ imps top env (PPi (Exp l _ doc _) n ty sc)

999999 = do let isn = nub (namesIn uvars ist ty ++ case sc of

10001000 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

10011001 _ -> [])

@@ -1057,8 +1057,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

10571057 pibind using [] sc = sc

10581058 pibind using (n:ns) sc

10591059 = case lookup n using of

1060− Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)

1061− Nothing -> PPi (Imp False Dynamic "") n Placeholder

1060+ Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)

1061+ Nothing -> PPi (Imp False Dynamic "" False) n Placeholder

10621062 (pibind using ns sc)

10631063

10641064-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+15−9

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

241241 | Search PTerm

242242 | CaseSplit Name PTerm

243243 | CaseSplitAt Bool Int Name

244+ | AddClauseFrom Bool Int Name

244245 | SetOpt Opt

245246 | UnsetOpt Opt

246247 | NOP

@@ -331,10 +332,12 @@ deriving instance Binary Static

331332-- Mark bindings with their explicitness, and laziness

332333data Plicity = Imp { plazy :: Bool,

333334 pstatic :: Static,

334− pdocstr :: String }

335+ pdocstr :: String,

336+ pparam :: Bool }

335337 | Exp { plazy :: Bool,

336338 pstatic :: Static,

337− pdocstr :: String }

339+ pdocstr :: String,

340+ pparam :: Bool }

338341 | Constraint { plazy :: Bool,

339342 pstatic :: Static,

340343 pdocstr :: String }

@@ -348,8 +351,9 @@ data Plicity = Imp { plazy :: Bool,

348351deriving instance Binary Plicity

349352!-}

350353

351−impl = Imp False Dynamic ""

352−expl = Exp False Dynamic ""

354+impl = Imp False Dynamic "" False

355+expl = Exp False Dynamic "" False

356+expl_param = Exp False Dynamic "" True

353357constraint = Constraint False Dynamic ""

354358tacimpl t = TacImp False Dynamic t ""

355359

@@ -916,7 +920,7 @@ prettyImp impl = prettySe 10

916920 else

917921 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

918922 prettySe 10 sc

919− prettySe p (PPi (Exp l s _) n ty sc)

923+ prettySe p (PPi (Exp l s _ _) n ty sc)

920924 | n `elem` allNamesIn sc || impl =

921925 let open = if l then text "|" <> lparen else lparen in

922926 bracket p 2 $

@@ -937,7 +941,7 @@ prettyImp impl = prettySe 10

937941 case s of

938942 Static -> text "[static]"

939943 _ -> empty

940− prettySe p (PPi (Imp l s _) n ty sc)

944+ prettySe p (PPi (Imp l s _ _) n ty sc)

941945 | impl =

942946 let open = if l then text "|" <> lbrace else lbrace in

943947 bracket p 2 $

@@ -1128,18 +1132,20 @@ showImp ist impl colour tm = se 10 [] tm where

11281132 se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++

11291133 " = " ++ se 10 bnd v ++

11301134 " in " ++ se 10 ((n, False):bnd) sc

1131− se p bnd (PPi (Exp l s _) n ty sc)

1135+ se p bnd (PPi (Exp l s _ param) n ty sc)

11321136 | n `elem` allNamesIn sc || impl

11331137 = bracket p 2 $

11341138 (if l then "|(" else "(") ++

11351139 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1136− ") " ++ st ++

1140+ ") " ++

1141+ (if (impl && param) then "P" else "") ++

1142+ st ++

11371143 "-> " ++ se 10 ((n, False):bnd) sc

11381144 | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc

11391145 where st = case s of

11401146 Static -> "[static] "

11411147 _ -> ""

1142− se p bnd (PPi (Imp l s _) n ty sc)

1148+ se p bnd (PPi (Imp l s _ _) n ty sc)

11431149 | impl = bracket p 2 $ (if l then "|{" else "{") ++

11441150 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

11451151 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

src/Idris/CaseSplit.hs+18−1

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.CaseSplit(split, splitOnLine, replaceSplits) where

3+module Idris.CaseSplit(split, splitOnLine, replaceSplits, getClause) where

55-- splitting a variable in a pattern clause

@@ -224,5 +224,22 @@ replaceSplits l ups = map (rep (expandBraces l)) ups

224224 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

225225 | otherwise = tm

226226

227+getClause :: Int -> -- ^ Line type is declared on

228+ Name -> -- ^ Function name

229+ FilePath -> -- ^ Source file name

230+ Idris String

231+getClause l fn fp = do ty <- getInternalApp fp l

232+ let ap = mkApp ty [1..]

233+ return (show fn ++ " " ++ ap ++

234+ "= ?" ++ show fn ++ "_rhs")

235+ where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)

236+ = "x" ++ show n ++ " " ++ mkApp sc ns

237+ mkApp (PPi (Exp _ _ _ False) n _ sc) ns

238+ = show n ++ " " ++ mkApp sc ns

239+ mkApp (PPi _ _ _ sc) ns = mkApp sc ns

240+ mkApp _ _ = ""

241+

242+

243+

227244

228245

src/Idris/ElabDecls.hs+17−11

@@ -52,9 +52,15 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

5252 do checkUndefined fc n

5353 ctxt <- getContext

5454 i <- getIState

55+

56+ -- Add user one, not implicitsed one

57+ addInternalApp (fc_fname fc) (fc_line fc) ty'

58+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) ty')

59+

5560 logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

5661 ty' <- addUsingConstraints syn fc ty'

5762 ty' <- implicit syn n ty'

63+

5864 let ty = addImpl i ty'

5965 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

6066 ((tyT, defer, is), log) <-

@@ -406,10 +412,10 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

406412 show fn ++ " (" ++ show ty ++ ")"

407413 putIState i)

408414

409− getImplB k (PPi (Imp l s _) n Placeholder sc)

415+ getImplB k (PPi (Imp l s _ _) n Placeholder sc)

410416 = getImplB k sc

411− getImplB k (PPi (Imp l s d) n ty sc)

412− = getImplB (\x -> k (PPi (Imp l s d) n ty x)) sc

417+ getImplB k (PPi (Imp l s d p) n ty sc)

418+ = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc

413419 getImplB k (PPi _ n ty sc)

414420 = getImplB k sc

415421 getImplB k _ = k

@@ -1244,8 +1250,8 @@ elabClass info syn doc fc constraints tn ps ds

12441250 return [PTy doc syn fc o m ty',

12451251 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

12461252

1247− getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

1248− getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

1253+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

1254+ getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc

12491255 getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

12501256 getMArgs _ = []

12511257

@@ -1262,14 +1268,14 @@ elabClass info syn doc fc constraints tn ps ds

12621268 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

12631269 rhsArgs [] _ = []

12641270

1265− insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

1271+ insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

12661272 = PPi p n ty (insertConstraint c sc)

12671273 insertConstraint c sc = PPi constraint (MN 0 "class") c sc

12681274

12691275 -- make arguments explicit and don't bind class parameters

1270− toExp ns e (PPi (Imp l s _) n ty sc)

1276+ toExp ns e (PPi (Imp l s _ p) n ty sc)

12711277 | n `elem` ns = toExp ns e sc

1272− | otherwise = PPi (e l s "") n ty (toExp ns e sc)

1278+ | otherwise = PPi (e l s "" p) n ty (toExp ns e sc)

12731279 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

12741280 toExp ns e sc = sc

12751281

@@ -1364,9 +1370,9 @@ elabInstance info syn fc cs n ps t expn ds

13641370 lamBind i (PPi _ n ty sc) sc'

13651371 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

13661372 lamBind i _ sc = sc

1367− methArgs i (PPi (Imp _ _ _) n ty sc)

1373+ methArgs i (PPi (Imp _ _ _ _) n ty sc)

13681374 = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1369− methArgs i (PPi (Exp _ _ _) n ty sc)

1375+ methArgs i (PPi (Exp _ _ _ _) n ty sc)

13701376 = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

13711377 methArgs i (PPi (Constraint _ _ _) n ty sc)

13721378 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

@@ -1393,7 +1399,7 @@ elabInstance info syn fc cs n ps t expn ds

13931399 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

13941400 conbind [] x = x

13951401

1396− coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

1402+ coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

13971403 coninsert cs sc = conbind cs sc

13981404

13991405 insertDefaults :: IState -> Name ->

src/Idris/IBC.hs+9−5

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 43

26+ibcVersion = 44

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -1008,16 +1008,18 @@ instance Binary Static where

10081008instance Binary Plicity where

10091009 put x

10101010 = case x of

1011− Imp x1 x2 x3 ->

1011+ Imp x1 x2 x3 x4 ->

10121012 do putWord8 0

10131013 put x1

10141014 put x2

10151015 put x3

1016− Exp x1 x2 x3 ->

1016+ put x4

1017+ Exp x1 x2 x3 x4 ->

10171018 do putWord8 1

10181019 put x1

10191020 put x2

10201021 put x3

1022+ put x4

10211023 Constraint x1 x2 x3 ->

10221024 do putWord8 2

10231025 put x1

@@ -1035,11 +1037,13 @@ instance Binary Plicity where

10351037 0 -> do x1 <- get

10361038 x2 <- get

10371039 x3 <- get

1038− return (Imp x1 x2 x3)

1040+ x4 <- get

1041+ return (Imp x1 x2 x3 x4)

10391042 1 -> do x1 <- get

10401043 x2 <- get

10411044 x3 <- get

1042− return (Exp x1 x2 x3)

1045+ x4 <- get

1046+ return (Exp x1 x2 x3 x4)

10431047 2 -> do x1 <- get

10441048 x2 <- get

10451049 x3 <- get

src/Idris/ParseExpr.hs+3−3

@@ -699,7 +699,7 @@ pi syn =

699699 doc <- option "" (docComment '^')

700700 symbol "->"

701701 sc <- expr syn

702− return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do

702+ return (bindList (PPi (Exp lazy st doc False)) xt sc)) <|> (do

703703 lchar '{'

704704 (do reserved "auto"

705705 when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"

@@ -722,13 +722,13 @@ pi syn =

722722 t <- expr' syn

723723 symbol "->"

724724 sc <- expr syn

725− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (

725+ return (PPi (Exp False Static "" False) (MN 42 "__pi_arg") t sc)) <|> (

726726 if implicitAllowed syn then do

727727 xt <- typeDeclList syn

728728 lchar '}'

729729 symbol "->"

730730 sc <- expr syn

731− return (bindList (PPi (Imp lazy st "")) xt sc)

731+ return (bindList (PPi (Imp lazy st "" False)) xt sc)

732732 else do fail "no implicit arguments allowed here"))

733733 <?> "dependent type signature"

734734

src/Idris/REPL.hs+23−1

@@ -140,8 +140,10 @@ processNetCmd stvar orig i h fn cmd

140140 processNet fn Reload =

141141 do let ist = orig { idris_options = idris_options i

142142 , idris_colourTheme = idris_colourTheme i

143+ , idris_colourRepl = False

143144 }

144− putIState orig

145+ putIState ist

146+ setErrContext True

145147 setOutH h

146148 setQuiet True

147149 setVerbose False

@@ -511,6 +513,26 @@ process h fn (CaseSplitAt updatefile l n)

511513 runIO $ copyFile fb fn

512514 else do ihputStrLn h (show res)

513515 ihputStrLn h new

516+process h fn (AddClauseFrom updatefile l n)

517+ = do src <- runIO $ readFile fn

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

519+ let indent = getIndent 0 (show n) tyline

520+ cl <- getClause l n fn

521+ -- add clause before first blank line in 'later'

522+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

523+ if updatefile then

524+ do let fb = fn ++ "~"

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

526+ ++ replicate indent ' ' ++

527+ cl ++ "\n" ++

528+ unlines rest)

529+ runIO $ copyFile fb fn

530+ else ihputStrLn h cl

531+ where

532+ getIndent i n [] = 0

533+ getIndent i n xs | take (length n) xs == n = i

534+ getIndent i n (x : xs) = getIndent (i + 1) n xs

535+

514536

515537

516538process h fn (Spec t)

src/Idris/REPLParser.hs+7−3

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

4545 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

4646 <|> try (do cmd ["proofs"]; eof; return Proofs)

4747 <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

48− <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

49− return (Just x))

50− eof; return (AddProof n))

5148 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

5249 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

5350 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

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

7875 n <- P.name;

7976 t <- P.fullExpr defaultSyntax;

8077 return (CaseSplit n t))

78+ <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;

79+ upd <- option False (do P.lchar '!'; return True)

80+ l <- P.natural; n <- P.name;

81+ return (AddClauseFrom upd (fromInteger l) n))

82+ <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

83+ return (Just x))

84+ eof; return (AddProof n))

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

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

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