6f462b8 · Idris-dev · git.iko.soy

CONTRIBUTORS+2−1

compare with master

unifiedsplit

@@ -3,10 +3,12 @@ Thanks to the following for their help and contributions:

3Ozgur Akgun

4Nicola Botta

5Edwin Brady

6+David Raymond Christiansen

6Jason Dagit

7Jason Dagit

7Cezar Ionescu

8Cezar Ionescu

8Irene Knapp

9Irene Knapp

9Mathnerd314

10Mathnerd314

11+Hannes Mehnert

10Mekeor Melire

12Mekeor Melire

11Melissa Mozifian

13Melissa Mozifian

12Dominic Mulligan

14Dominic Mulligan

@@ -20,4 +22,3 @@ Dirk Ullrich

20Leif Warner

22Leif Warner

21Daniel Waterworth

23Daniel Waterworth

22Jonas Westerlund

24Jonas Westerlund

23−David Raymond Christiansen

contribs/lib/._simpleparser.idrdeleted

Binary file not shown.

contribs/lib/SQLite3/._Makefiledeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlexpr.idrdeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlite3.idrdeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlite3api.cdeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlite3api.hdeleted

Binary file not shown.

contribs/lib/SQLite3/._testunit.idrdeleted

Binary file not shown.

effects/Effect/State.idr+5

@@ -29,3 +29,8 @@ update : (x -> x) -> Eff m [STATE x] ()

29update f = do val <- get

30 put (f val)

31

32+updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()

33+updateM f = do val <- get

34+ putM (f val)

35+

36+

git-credential-osxkeychaindeleted

Binary file not shown.

idris.cabal+1−1

@@ -77,7 +77,7 @@ Executable idris

77 Core.CaseTree, Core.Constraints,

78

79 Idris.AbsSyntax, Idris.AbsSyntaxTree,

80− Idris.Parser, Idris.REPL,

80+ Idris.Parser, Idris.Help, Idris.REPL,

81 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

82 Idris.Delaborate, Idris.Primitives, Idris.Imports,

83 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

lib/Prelude.idr−1

@@ -268,7 +268,6 @@ data Mode = Read | Write | ReadWrite

268partial

269openFile : String -> Mode -> IO File

270openFile f m = fopen f (modeStr m) where

271− modeStr : Mode -> String

272 modeStr Read = "r"

271 modeStr Read = "r"

273 modeStr Write = "w"

272 modeStr Write = "w"

274 modeStr ReadWrite = "r+"

273 modeStr ReadWrite = "r+"

lib/Prelude/Strings.idr+1−1

@@ -36,7 +36,7 @@ strM x with (choose (not (x == "")))

36unpack : String -> List Char

37unpack s with (strM s)

38 unpack "" | StrNil = []

39− unpack (strCons x xs) | (StrCons _ xs) = x :: unpack xs

39+ unpack (strCons x xs) | (StrCons x xs) = x :: unpack xs

40

41pack : List Char -> String

42pack [] = ""

src/Idris/AbsSyntax.hs+33

@@ -914,6 +914,39 @@ aiFn inpat expat ist fc f as

914 | n == n' = Just (t, reverse acc ++ gs)

915 find n (g : gs) acc = find n gs (g : acc)

916

917+-- replace non-linear occurrences with _

918+stripLinear :: IState -> PTerm -> PTerm

919+stripLinear i tm = evalState (sl tm) [] where

920+ sl :: PTerm -> State [Name] PTerm

921+ sl (PRef fc f)

922+ | (_:_) <- lookupTy Nothing f (tt_ctxt i)

923+ = return $ PRef fc f

924+ | otherwise = do ns <- get

925+ trace (show (f, ns)) $ if (f `elem` ns)

926+ then return Placeholder

927+ else do put (f : ns)

928+ return (PRef fc f)

929+ sl (PPatvar fc f)

930+ = do ns <- get

931+ if (f `elem` ns)

932+ then return Placeholder

933+ else do put (f : ns)

934+ return (PPatvar fc f)

935+ sl (PApp fc fn args) = do fn' <- sl fn

936+ args' <- mapM slA args

937+ return $ PApp fc fn' args'

938+ where slA (PImp p l n t d) = do t' <- sl t

939+ return $ PImp p l n t' d

940+ slA (PExp p l t d) = do t' <- sl t

941+ return $ PExp p l t' d

942+ slA (PConstraint p l t d)

943+ = do t' <- sl t

944+ return $ PConstraint p l t' d

945+ slA (PTacImplicit p l n sc t d)

946+ = do t' <- sl t

947+ return $ PTacImplicit p l n sc t' d

948+ sl x = return x

949+

917mkPApp fc a f [] = f

950mkPApp fc a f [] = f

918mkPApp fc a f as = let rest = drop a as in

951mkPApp fc a f as = let rest = drop a as in

919 appRest fc (PApp fc f (take a as)) rest

952 appRest fc (PApp fc f (take a as)) rest

src/Idris/Completion.hs+14−35

@@ -6,6 +6,7 @@ import Core.TT

6import Core.CoreParser (opChars)

7

8import Idris.AbsSyntaxTree

9+import Idris.Help

9

10

10import Control.Monad.State.Strict

11import Control.Monad.State.Strict

11

12

@@ -14,40 +15,11 @@ import Data.Maybe

14

15

15import System.Console.Haskeline

16import System.Console.Haskeline

16

17

17−-- TODO: add specific classes of identifiers to complete, fx metavariables

18+

18−-- | A specification of the arguments that REPL commands can take

19+fst4 :: (a, b, c, d) -> a

19−data CmdArg = ExprArg -- ^ The command takes an expression

20+fst4 (a, b, c, d) = a

20− | NameArg -- ^ The command takes a name

21+

21− | FileArg -- ^ The command takes a file

22+commands = concatMap fst4 help

22− | ModuleArg -- ^ The command takes a module name

23− | OptionArg -- ^ The command takes an option

24− | MetaVarArg -- ^ The command takes a metavariable

25−

26−-- | Information about how to complete the various commands

27−cmdArgs :: [(String, CmdArg)]

28−cmdArgs = [ (":t", ExprArg)

29− , (":miss", NameArg)

30− , (":missing", NameArg)

31− , (":i", NameArg)

32− , (":info", NameArg)

33− , (":total", NameArg)

34− , (":l", FileArg)

35− , (":load", FileArg)

36− , (":m", ModuleArg) -- NOTE: Argumentless form is a different command

37− , (":p", MetaVarArg)

38− , (":prove", MetaVarArg)

39− , (":a", NameArg)

40− , (":addproof", NameArg)

41− , (":rmproof", NameArg)

42− , (":showproof", NameArg)

43− , (":c", FileArg)

44− , (":compile", FileArg)

45− , (":js", FileArg)

46− , (":javascript", FileArg)

47− , (":set", OptionArg)

48− , (":unset", OptionArg)

49− ]

50−commands = map fst cmdArgs

51

23

52-- | A specification of the arguments that tactics can take

24-- | A specification of the arguments that tactics can take

53data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

25data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

@@ -124,15 +96,22 @@ completeOption = completeWord Nothing " \t" completeOpt

124isWhitespace :: Char -> Bool

96isWhitespace :: Char -> Bool

125isWhitespace = (flip elem) " \t\n"

97isWhitespace = (flip elem) " \t\n"

126

98

99+lookupInHelp :: String -> Maybe CmdArg

100+lookupInHelp cmd = lookupInHelp' cmd help

101+ where lookupInHelp' cmd ((cmds, _, _, arg):xs) | elem cmd cmds = Just arg

102+ | otherwise = lookupInHelp' cmd xs

103+ lookupInHelp' cmd [] = Nothing

104+

127-- | Get the completion function for a particular command

105-- | Get the completion function for a particular command

128completeCmd :: String -> CompletionFunc Idris

106completeCmd :: String -> CompletionFunc Idris

129−completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs

107+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd

130 where completeArg FileArg = completeFilename (prev, next)

108 where completeArg FileArg = completeFilename (prev, next)

131 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name

109 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name

132 completeArg OptionArg = completeOption (prev, next)

110 completeArg OptionArg = completeOption (prev, next)

133 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

111 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

134 completeArg ExprArg = completeExpr [] (prev, next)

112 completeArg ExprArg = completeExpr [] (prev, next)

135 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

113 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

114+ completeArg NoArg = noCompletion (prev, next)

136 completeCmdName = return $ ("", completeWith commands cmd)

115 completeCmdName = return $ ("", completeWith commands cmd)

137

116

138-- | Complete REPL commands and defined identifiers

117-- | Complete REPL commands and defined identifiers

src/Idris/ElabDecls.hs+1−1

@@ -548,7 +548,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

548 [t] -> t

549 _ -> []

550 let params = getParamsInType i [] fn_is fn_ty

551− let lhs = addImplPat i (propagateParams params lhs_in)

551+ let lhs = stripLinear i $ addImplPat i (propagateParams params lhs_in)

552 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)

553 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

554 ((lhs', dlhs, []), _) <-

src/Idris/ElabTerm.hs+16−12

@@ -198,19 +198,23 @@ elab ist info pattern tcgen fn tm

198 trySeq' deferr (x : xs)

199 = try' (elab' ina x) (trySeq' deferr xs) True

200 elab' ina (PPatvar fc n) | pattern = patvar n

201+-- = do env <- get_env

202+-- case lookup n env of

203+-- Just (PVar _) -> elab' ina Placeholder

204+-- _ -> patvar n

201 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

205 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

202− = do ctxt <- get_context

206+ = do ctxt <- get_context

203− let iscon = isConName Nothing n ctxt

207+ env <- get_env

204− let defined = case lookupTy Nothing n ctxt of

208+ let defined = case lookupTy Nothing n ctxt of

205− [] -> False

209+ [] -> False

206− _ -> True

210+ _ -> True

207− -- this is to stop us resolve type classes recursively

211+ -- this is to stop us resolve type classes recursively

208− -- trace (show (n, guarded)) $

212+ -- trace (show (n, guarded)) $

209− if (tcname n && ina) then erun fc $ patvar n

213+ if (tcname n && ina) then erun fc $ patvar n

210− else if (defined && not guarded)

214+ else if (defined && not guarded)

211− then do apply (Var n) []; solve

215+ then do apply (Var n) []; solve

212− else try (do apply (Var n) []; solve)

216+ else try (do apply (Var n) []; solve)

213− (patvar n)

217+ (patvar n)

214 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

218 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

215 [] -> False

219 [] -> False

216 _ -> True

220 _ -> True

src/Idris/Help.hsnew file+36

@@ -0,0 +1,36 @@

1+module Idris.Help (CmdArg(..), help) where

2+

3+data CmdArg = ExprArg -- ^ The command takes an expression

4+ | NameArg -- ^ The command takes a name

5+ | FileArg -- ^ The command takes a file

6+ | ModuleArg -- ^ The command takes a module name

7+ | OptionArg -- ^ The command takes an option

8+ | MetaVarArg -- ^ The command takes a metavariable

9+ | NoArg -- ^ No completion yet

10+

11+

12+help :: [([String], String, String, CmdArg)]

13+help =

14+ [ (["<expr>"], "", "Evaluate an expression", NoArg),

15+ ([":t"], "<expr>", "Check the type of an expression", ExprArg),

16+ ([":miss", ":missing"], "<name>", "Show missing clauses", NameArg),

17+ ([":i", ":info"], "<name>", "Display information about a type class", NameArg),

18+ ([":total"], "<name>", "Check the totality of a name", NameArg),

19+ ([":r",":reload"], "", "Reload current file", NoArg),

20+ ([":l",":load"], "<filename>", "Load a new file", FileArg),

21+ ([":m",":module"], "<module>", "Import an extra module", ModuleArg), -- NOTE: dragons

22+ ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL", NoArg),

23+ ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)", MetaVarArg),

24+ ([":p",":prove"], "<name>", "Prove a metavariable", MetaVarArg),

25+ ([":a",":addproof"], "<name>", "Add proof to source file", NameArg),

26+ ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),

27+ ([":showproof"], "<name>", "Show proof", NameArg),

28+ ([":proofs"], "", "Show available proofs", NoArg),

29+ ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),

30+ ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),

31+ ([":exec",":execute"], "", "Compile to an executable and run", NoArg),

32+ ([":?",":h",":help"], "", "Display this help text", NoArg),

33+ ([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),

34+ ([":unset"], "<option>", "Unset an option", OptionArg),

35+ ([":q",":quit"], "", "Exit the Idris system", NoArg)

36+ ]

src/Idris/Prover.hs+2

@@ -20,6 +20,7 @@ import System.Console.Haskeline.History

20import Control.Monad.State

21

22import Util.Pretty

23+import Debug.Trace

23

24

24prover :: Bool -> Name -> Idris ()

25prover :: Bool -> Name -> Idris ()

25prover lit x =

26prover lit x =

@@ -159,6 +160,7 @@ ploop d prompt prf e h

159 return (False, e, True, prf)

160 return (False, e, True, prf)

160 Right tac -> do (_, e) <- elabStep e saveState

161 Right tac -> do (_, e) <- elabStep e saveState

161 (_, st) <- elabStep e (runTac True i tac)

162 (_, st) <- elabStep e (runTac True i tac)

163+-- trace (show (problems (proof st))) $

162 return (True, st, False, prf ++ [step]))

164 return (True, st, False, prf ++ [step]))

163 (\err -> do iputStrLn (show err)

165 (\err -> do iputStrLn (show err)

164 return (False, e, False, prf))

166 return (False, e, False, prf))

src/Idris/REPL.hs+6−26

@@ -16,6 +16,7 @@ import Idris.Primitives

16import Idris.Coverage

17import Idris.UnusedArgs

18import Idris.Docs

19+import Idris.Help

19import Idris.Completion

20import Idris.Completion

20

21

21import Paths_idris

22import Paths_idris

@@ -418,8 +419,9 @@ showTotalN i n = case lookupTotal n (tt_ctxt i) of

418displayHelp = let vstr = showVersion version in

419displayHelp = let vstr = showVersion version in

419 "\nIdris version " ++ vstr ++ "\n" ++

420 "\nIdris version " ++ vstr ++ "\n" ++

420 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

421 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

422+ concatMap cmdInfo helphead ++

421 concatMap cmdInfo help

423 concatMap cmdInfo help

422− where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text

424+ where cmdInfo (cmds, args, text, _) = " " ++ col 16 12 (showSep " " cmds) args text

423 col c1 c2 l m r =

425 col c1 c2 l m r =

424 l ++ take (c1 - length l) (repeat ' ') ++

426 l ++ take (c1 - length l) (repeat ' ') ++

425 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

427 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

@@ -469,31 +471,9 @@ parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

469parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

471parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

470parseArgs (n:ns) = Filename n : (parseArgs ns)

472parseArgs (n:ns) = Filename n : (parseArgs ns)

471

473

472−help =

474+helphead =

473− [ (["Command"], "Arguments", "Purpose"),

475+ [ (["Command"], "Arguments", "Purpose", ""),

474− ([""], "", ""),

475− (["<expr>"], "", "Evaluate an expression"),

476+ ([""], "", "", "")

476− ([":t"], "<expr>", "Check the type of an expression"),

477− ([":miss", ":missing"], "<name>", "Show missing clauses"),

478− ([":i", ":info"], "<name>", "Display information about a type class"),

479− ([":total"], "<name>", "Check the totality of a name"),

480− ([":r",":reload"], "", "Reload current file"),

481− ([":l",":load"], "<filename>", "Load a new file"),

482− ([":m",":module"], "<module>", "Import an extra module"),

483− ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

484− ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

485− ([":p",":prove"], "<name>", "Prove a metavariable"),

486− ([":a",":addproof"], "<name>", "Add proof to source file"),

487− ([":rmproof"], "<name>", "Remove proof from proof stack"),

488− ([":showproof"], "<name>", "Show proof"),

489− ([":proofs"], "", "Show available proofs"),

490− ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

491− ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),

492− ([":exec",":execute"], "", "Compile to an executable and run"),

493− ([":?",":h",":help"], "", "Display this help text"),

494− ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),

495− ([":unset"], "<option>", "Unset an option"),

496− ([":q",":quit"], "", "Exit the Idris system")

497 ]

477 ]

498

478

499

479

test/reg005/reg005.idr+2−2

@@ -20,7 +20,7 @@ rle [] = REnd

20rle (x :: xs) with (rle xs)

21 rle (x :: Vect.Nil) | REnd = RChar O x REnd

22 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

23− rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p

23+ rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl

24 = RChar (S n) x rs

25 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing

26 = RChar O x (RChar n y rs)

@@ -28,7 +28,7 @@ rle (x :: xs) with (rle xs)

28compress : Vect Char n -> String

29compress xs with (rle xs)

30 compress Nil | REnd = ""

31− compress (rep (S n) x ++ xs) | RChar n x rs

31+ compress (rep (S n) x ++ xs) | RChar _ _ rs

32 = let ni : Int = cast (S n) in

33 show ni ++ show x ++ compress xs

34

test/reg010/expectednew file+4

@@ -0,0 +1,4 @@

1+reg010.idr:5:Can't unify P x with P y

2+

3+Specifically:

4+ Can't unify x with y

test/reg010/reg010.idrnew file+5

@@ -0,0 +1,5 @@

1+module usubst

2+

3+total unsafeSubst : (P : a -> Type) -> (x : a) -> (y : a) -> P x -> P y

4+unsafeSubst P x y px with (O)

5+ unsafeSubst P x x px | _ = px

test/reg010/runnew file+2

@@ -0,0 +1,2 @@

1+#!/bin/bash

2+idris $@ reg010.idr --check