89a055e · Idris-dev · git.iko.soy

CONTRIBUTORS+2−1

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

33Ozgur Akgun

44Nicola Botta

55Edwin Brady

6+David Raymond Christiansen

67Jason Dagit

78Cezar Ionescu

89Irene Knapp

910Mathnerd314

11+Hannes Mehnert

1012Mekeor Melire

1113Melissa Mozifian

1214Dominic Mulligan

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

2022Leif Warner

2123Daniel Waterworth

2224Jonas 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] ()

2929update f = do val <- get

3030 put (f val)

3131

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

@@ -85,7 +85,7 @@ Executable idris

8585 Core.CaseTree, Core.Constraints,

8686

8787 Idris.AbsSyntax, Idris.AbsSyntaxTree,

88− Idris.Parser, Idris.REPL,

88+ Idris.Parser, Idris.Help, Idris.REPL,

8989 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

9090 Idris.Delaborate, Idris.Primitives, Idris.Imports,

9191 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

lib/Prelude.idr−1

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

268268partial

269269openFile : String -> Mode -> IO File

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

271− modeStr : Mode -> String

272271 modeStr Read = "r"

273272 modeStr Write = "w"

274273 modeStr ReadWrite = "r+"

lib/Prelude/Strings.idr+1−1

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

3636unpack : String -> List Char

3737unpack s with (strM s)

3838 unpack "" | StrNil = []

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

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

4040

4141pack : List Char -> String

4242pack [] = ""

rts/idris_rts.c+11−4

@@ -106,12 +106,19 @@ void* allocate(VM* vm, size_t size, int outerlock) {

106106 if ((size & 7)!=0) {

107107 size = 8 + ((size >> 3) << 3);

108108 }

109− if (vm -> heap_next + size < vm -> heap_end) {

110− vm->allocations += size + sizeof(size_t);

109+

110+ size_t chunk_size = size + sizeof(size_t);

111+

112+ if (vm -> heap_next + chunk_size < vm -> heap_end) {

113+ vm->allocations += chunk_size;

111114 void* ptr = (void*)(vm->heap_next + sizeof(size_t));

112− *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

113− vm -> heap_next += size + sizeof(size_t);

115+ *((size_t*)(vm->heap_next)) = chunk_size;

116+ vm -> heap_next += chunk_size;

117+

118+ assert(vm->heap_next <= vm->heap_end);

119+

114120 memset(ptr, 0, size);

121+

115122 if (lock) { // not message passing

116123 pthread_mutex_unlock(&vm->alloc_lock);

117124 }

src/Idris/AbsSyntax.hs+33

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

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

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

916916

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+

917950mkPApp fc a f [] = f

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

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

src/Idris/Completion.hs+14−35

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

66import Core.CoreParser (opChars)

77

88import Idris.AbsSyntaxTree

9+import Idris.Help

910

1011import Control.Monad.State.Strict

1112

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

1415

1516import System.Console.Haskeline

1617

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

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

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

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

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

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

18+

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

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

21+

22+commands = concatMap fst4 help

5123

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

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

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

12496isWhitespace :: Char -> Bool

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

12698

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+

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

128106completeCmd :: 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

130108 where completeArg FileArg = completeFilename (prev, next)

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

132110 completeArg OptionArg = completeOption (prev, next)

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

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

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

114+ completeArg NoArg = noCompletion (prev, next)

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

137116

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

548548 [t] -> t

549549 _ -> []

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

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

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

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

src/Idris/ElabTerm.hs+18−13

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

198198 trySeq' deferr (x : xs)

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

200200 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

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

202− = do ctxt <- get_context

203− let iscon = isConName Nothing n ctxt

204− let defined = case lookupTy Nothing n ctxt of

205− [] -> False

206− _ -> True

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

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

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

210− else if (defined && not guarded)

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

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

213− (patvar n)

206+ = do ctxt <- get_context

207+ env <- get_env

208+ let defined = case lookupTy Nothing n ctxt of

209+ [] -> False

210+ _ -> True

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

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

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

214+ else if (defined && not guarded)

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

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

217+ (patvar n)

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

215219 [] -> False

216220 _ -> True

@@ -533,7 +537,8 @@ pruneByType (P _ n _) c as

533537

534538 typeHead var f f'

535539 = case lookupTy Nothing f' c of

536− [ty] -> case unApply (getRetTy ty) of

540+ [ty] -> let ty' = normalise c [] ty in

541+ case unApply (getRetTy ty') of

537542 (P _ ftyn _, _) -> ftyn == f

538543 (V _, _) -> var -- keep, variable

539544 _ -> False

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

2020import Control.Monad.State

2121

2222import Util.Pretty

23+import Debug.Trace

2324

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

2526prover lit x =

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

159160 return (False, e, True, prf)

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

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

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

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

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

164166 return (False, e, False, prf))

src/Idris/REPL.hs+6−26

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

1616import Idris.Coverage

1717import Idris.UnusedArgs

1818import Idris.Docs

19+import Idris.Help

1920import Idris.Completion

2021

2122import Paths_idris

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

418419displayHelp = let vstr = showVersion version in

419420 "\nIdris version " ++ vstr ++ "\n" ++

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

422+ concatMap cmdInfo helphead ++

421423 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

423425 col c1 c2 l m r =

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

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

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

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

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

471473

472−help =

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

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

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

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

474+helphead =

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

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

497477 ]

498478

499479

test/reg005/reg005.idr+2−2

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

2020rle (x :: xs) with (rle xs)

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

2222 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

2424 = RChar (S n) x rs

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

2626 = RChar O x (RChar n y rs)

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

2828compress : Vect Char n -> String

2929compress xs with (rle xs)

3030 compress Nil | REnd = ""

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

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

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

3333 show ni ++ show x ++ compress xs

3434

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