f8f5f17 · Idris-dev · git.iko.soy

CONTRIBUTORS+1−1

compare with master

unifiedsplit

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

20Leif Warner

21Daniel Waterworth

22Jonas Westerlund

23−

23+David Raymond Christiansen

contribs/tool-support/vim/syntax/idris.vim+3−1

@@ -4,7 +4,7 @@

4" highlighter to support idris.

5"

6" author: raichoo (raichoo@googlemail.com)

7−" date: Mar 11 2013

7+" date: Mar 12 2013

8

9syn match idrisModule "\<$module\|namespace$\>"

10syn match idrisImport "\<import\>"

@@ -26,6 +26,7 @@ syn match idrisLineComment "---*$[^-!#$%&\*\+./<=>\?@\\^|~].*$\?$"

26syn match idrisMetaVar "?[a-z][A-Za-z0-9_]\+"

27syn match idrisLink "%$lib\|link\|include$"

28syn match idrisDirective "%$access\|default\|assert_total$"

29+syn match idrisDSL "$lambda\|variable\|\index_first\|index_next$"

29syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+

30syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+

30syn region idrisBlockComment start="{-" end="-}"

31syn region idrisBlockComment start="{-" end="-}"

31syn region idrisProofBlock start="$default\s\+$\?$proof\|tactics$ *{" end="}" contains=idrisTactic

32syn region idrisProofBlock start="$default\s\+$\?$proof\|tactics$ *{" end="}" contains=idrisTactic

@@ -40,6 +41,7 @@ highlight def link idrisImport Structure

40highlight def link idrisModule Structure

41highlight def link idrisModule Structure

41highlight def link idrisStructure Structure

42highlight def link idrisStructure Structure

42highlight def link idrisStatement Statement

43highlight def link idrisStatement Statement

44+highlight def link idrisDSL Statement

43highlight def link idrisBlock Statement

45highlight def link idrisBlock Statement

44highlight def link idrisAnnotation Statement

46highlight def link idrisAnnotation Statement

45highlight def link idrisSyntax Statement

47highlight def link idrisSyntax Statement

lib/Uninhabited.idrnew file+12

@@ -0,0 +1,12 @@

1+module Uninhabited

2+

3+class Uninhabited t where

4+ total uninhabited : t -> _|_

5+

6+instance Uninhabited (Fin O) where

7+ uninhabited fO impossible

8+ uninhabited (fS f) impossible

9+

10+instance Uninhabited (O = S n) where

11+ uninhabited refl impossible

12+

lib/base.ipkg+2

@@ -15,6 +15,8 @@ modules = Builtins, Prelude, IO, System,

15

16 Decidable.Equality,

17

18+ Uninhabited,

19+

18 Language.Reflection,

20 Language.Reflection,

19

21

20 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

22 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

src/Core/CoreParser.hs+6−3

@@ -1,7 +1,7 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

2

3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,

4− idrisLexer, maybeWithNS, pDocComment) where

4+ idrisLexer, maybeWithNS, pDocComment, opChars) where

5

6import Core.TT

7

@@ -39,8 +39,11 @@ idrisDef = haskellDef {

39 "Bits8", "Bits16", "Bits32", "Bits64"]

40 }

41

42+-- | The characters allowed in operator names

43+opChars = ":!#$%&*+./<=>?@\\^|-~"

44+

42−iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

45+iOpStart = oneOf opChars

43−iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

46+iOpLetter = oneOf opChars

44-- <|> letter

47-- <|> letter

45

48

46idrisLexer :: TokenParser a

49idrisLexer :: TokenParser a

src/Idris/Completion.hs+17−5

@@ -3,6 +3,7 @@ module Idris.Completion (replCompletion, proverCompletion) where

3

4import Core.Evaluate (ctxtAlist)

5import Core.TT

6+import Core.CoreParser (opChars)

6

7

7import Idris.AbsSyntaxTree

8import Idris.AbsSyntaxTree

8

9

@@ -20,6 +21,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression

20 | FileArg -- ^ The command takes a file

21 | FileArg -- ^ The command takes a file

21 | ModuleArg -- ^ The command takes a module name

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

22 | OptionArg -- ^ The command takes an option

23 | OptionArg -- ^ The command takes an option

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

23

25

24-- | Information about how to complete the various commands

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

25cmdArgs :: [(String, CmdArg)]

27cmdArgs :: [(String, CmdArg)]

@@ -32,8 +34,8 @@ cmdArgs = [ (":t", ExprArg)

32 , (":l", FileArg)

34 , (":l", FileArg)

33 , (":load", FileArg)

35 , (":load", FileArg)

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

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

35− , (":p", NameArg)

37+ , (":p", MetaVarArg)

36− , (":prove", NameArg)

38+ , (":prove", MetaVarArg)

37 , (":a", NameArg)

39 , (":a", NameArg)

38 , (":addproof", NameArg)

40 , (":addproof", NameArg)

39 , (":rmproof", NameArg)

41 , (":rmproof", NameArg)

@@ -80,11 +82,15 @@ nameString _ = Nothing

80

82

81-- FIXME: Respect module imports

83-- FIXME: Respect module imports

82-- | Get the user-visible names from the current interpreter state.

84-- | Get the user-visible names from the current interpreter state.

83−names :: Idris[String]

85+names :: Idris [String]

84names = do i <- get

86names = do i <- get

85 let ctxt = tt_ctxt i

87 let ctxt = tt_ctxt i

86 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt

88 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt

87

89

90+metavars :: Idris [String]

91+metavars = do i <- get

92+ return . map (show . nsroot) $ idris_metavars i \\ primDefs

93+

88

94

89modules :: Idris [String]

95modules :: Idris [String]

90modules = do i <- get

96modules = do i <- get

@@ -97,14 +103,19 @@ completeWith ns n = if uniqueExists

97 then [simpleCompletion n]

103 then [simpleCompletion n]

98 else map simpleCompletion prefixMatches

104 else map simpleCompletion prefixMatches

99 where prefixMatches = filter (isPrefixOf n) ns

105 where prefixMatches = filter (isPrefixOf n) ns

100− uniqueExists = n `elem` prefixMatches

106+ uniqueExists = [n] == prefixMatches

101

107

102completeName :: [String] -> String -> Idris [Completion]

108completeName :: [String] -> String -> Idris [Completion]

103completeName extra n = do ns <- names

109completeName extra n = do ns <- names

104 return $ completeWith (extra ++ ns) n

110 return $ completeWith (extra ++ ns) n

105

111

106completeExpr :: [String] -> CompletionFunc Idris

112completeExpr :: [String] -> CompletionFunc Idris

107−completeExpr extra = completeWord Nothing " \t" (completeName extra)

113+completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)

114+

115+completeMetaVar :: CompletionFunc Idris

116+completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

117+ where completeM m = do mvs <- metavars

118+ return $ completeWith mvs m

108

119

109completeOption :: CompletionFunc Idris

120completeOption :: CompletionFunc Idris

110completeOption = completeWord Nothing " \t" completeOpt

121completeOption = completeWord Nothing " \t" completeOpt

@@ -121,6 +132,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo

121 completeArg OptionArg = completeOption (prev, next)

132 completeArg OptionArg = completeOption (prev, next)

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

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

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

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

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

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

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

125

137

126-- | Complete REPL commands and defined identifiers

138-- | Complete REPL commands and defined identifiers

src/Idris/Coverage.hs+5−3

@@ -569,8 +569,8 @@ checkMP ist i mp = if i > 0

569 x -> error (show x)

570 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

571 = Total []

572− tryPath desc path (e@(f, []) : es) arg

572+ tryPath desc path (e@(f, args) : es) arg

573− | e `elem` es = Partial (Mutual [f])

573+ | e `elem` es && allNothing args = Partial (Mutual [f])

574 tryPath desc path (e@(f, nextargs) : es) arg

575 | Just d <- lookup e path

576 = if desc > 0

@@ -587,7 +587,7 @@ checkMP ist i mp = if i > 0

587 -- rest definitely terminates without

588 -- any cycles with route so far,

589 -- then we might yet be total

590− case collapse (map (tryPath (-10000) ((e, desc):path) es)

590+ case collapse (map (tryPath (-10000) ((e, 0):path) es)

591 [0..length nextargs - 1]) of

592 Total _ -> return Unchecked

593 x -> return x

@@ -607,6 +607,8 @@ checkMP ist i mp = if i > 0

607 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

608 | otherwise = Unchecked

609

610+allNothing xs = null (collapseNothing (zip xs [0..]))

611+

610collapseNothing ((Nothing, _) : xs)

612collapseNothing ((Nothing, _) : xs)

611 = filter (\ (x, _) -> case x of

613 = filter (\ (x, _) -> case x of

612 Nothing -> False

614 Nothing -> False

src/Idris/ElabTerm.hs+1−2

@@ -477,7 +477,6 @@ elab ist info pattern tcgen fn tm

477 where elabArg n t

478 = do hs <- get_holes

479 tm <- get_term

480− t' <- insertCoerce ina t

481 failed' <- -- trace (show (n, t, hs, tm)) $

480 failed' <- -- trace (show (n, t, hs, tm)) $

482 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

481 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

483 case n `elem` hs of

482 case n `elem` hs of

@@ -485,7 +484,7 @@ elab ist info pattern tcgen fn tm

485-- if r

484-- if r

486-- then try (do focus n; elabE ina t; return failed)

485-- then try (do focus n; elabE ina t; return failed)

487-- (return ((n,(lazy, t)):failed))

486-- (return ((n,(lazy, t)):failed))

488− do focus n; elab' ina t'; return failed

487+ do focus n; elabE ina t; return failed

489 False -> return failed

488 False -> return failed

490 elabArgs ina failed fc r ns args

489 elabArgs ina failed fc r ns args

491

490

src/Idris/Parser.hs+1

@@ -213,6 +213,7 @@ openBlock = do lchar '{'

213closeBlock :: IParser ()

214closeBlock = do ist <- getState

215 bs <- case brace_stack ist of

216+ [] -> eof >> return []

216 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])

217 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])

217 Just lvl : xs -> (do i <- indent

218 Just lvl : xs -> (do i <- indent

218 inp <- getInput

219 inp <- getInput