f8f5f17 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of http://githib.com/edwinb/Idris-dev

commitf8f5f17c7e02e6cbfad5a7dd5355aabfe048ee02 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateWed 13 Mar 2013, 02:29 (14 years ago) parent1b46872 9841e2a

9 files changed+48−15

compare with master

unifiedsplit

CONTRIBUTORS+1−1 contribs/tool-support/vim/syntax/idris.vim+3−1 lib/Uninhabited.idr+12 lib/base.ipkg+2 src/Core/CoreParser.hs+6−3 src/Idris/Completion.hs+17−5 src/Idris/Coverage.hs+5−3 src/Idris/ElabTerm.hs+1−2 src/Idris/Parser.hs+1

CONTRIBUTORS+1−1

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

2020Leif Warner

2121Daniel Waterworth

2222Jonas Westerlund

23−

23+David Raymond Christiansen

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

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

44" highlighter to support idris.

55"

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

7−" date: Mar 11 2013

7+" date: Mar 12 2013

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

1010syn match idrisImport "\<import\>"

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

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

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

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

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

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

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

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

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

4041highlight def link idrisModule Structure

4142highlight def link idrisStructure Structure

4243highlight def link idrisStatement Statement

44+highlight def link idrisDSL Statement

4345highlight def link idrisBlock Statement

4446highlight def link idrisAnnotation Statement

4547highlight def link idrisSyntax Statement

lib/Uninhabited.idrnew file+12

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

1+module Uninhabited

3+class Uninhabited t where

4+ total uninhabited : t -> _|_

6+instance Uninhabited (Fin O) where

7+ uninhabited fO impossible

8+ uninhabited (fS f) impossible

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,

1515

1616 Decidable.Equality,

1717

18+ Uninhabited,

19+

1820 Language.Reflection,

1921

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

src/Core/CoreParser.hs+6−3

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

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

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

4− idrisLexer, maybeWithNS, pDocComment) where

4+ idrisLexer, maybeWithNS, pDocComment, opChars) where

66import Core.TT

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

3939 "Bits8", "Bits16", "Bits32", "Bits64"]

4040 }

4141

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

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

42+-- | The characters allowed in operator names

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

44+

45+iOpStart = oneOf opChars

46+iOpLetter = oneOf opChars

4447-- <|> letter

4548

4649idrisLexer :: TokenParser a

src/Idris/Completion.hs+17−5

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

44import Core.Evaluate (ctxtAlist)

55import Core.TT

6+import Core.CoreParser (opChars)

78import Idris.AbsSyntaxTree

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

2021 | FileArg -- ^ The command takes a file

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

2223 | OptionArg -- ^ The command takes an option

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

2325

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

2527cmdArgs :: [(String, CmdArg)]

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

3234 , (":l", FileArg)

3335 , (":load", FileArg)

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

35− , (":p", NameArg)

36− , (":prove", NameArg)

37+ , (":p", MetaVarArg)

38+ , (":prove", MetaVarArg)

3739 , (":a", NameArg)

3840 , (":addproof", NameArg)

3941 , (":rmproof", NameArg)

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

8082

8183-- FIXME: Respect module imports

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

83−names :: Idris[String]

85+names :: Idris [String]

8486names = do i <- get

8587 let ctxt = tt_ctxt i

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

8789

90+metavars :: Idris [String]

91+metavars = do i <- get

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

93+

8894

8995modules :: Idris [String]

9096modules = do i <- get

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

97103 then [simpleCompletion n]

98104 else map simpleCompletion prefixMatches

99105 where prefixMatches = filter (isPrefixOf n) ns

100− uniqueExists = n `elem` prefixMatches

106+ uniqueExists = [n] == prefixMatches

101107

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

103109completeName extra n = do ns <- names

104110 return $ completeWith (extra ++ ns) n

105111

106112completeExpr :: [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

108119

109120completeOption :: CompletionFunc Idris

110121completeOption = completeWord Nothing " \t" completeOpt

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

121132 completeArg OptionArg = completeOption (prev, next)

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

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

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

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

125137

126138-- | Complete REPL commands and defined identifiers

src/Idris/Coverage.hs+5−3

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

569569 x -> error (show x)

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

571571 = Total []

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

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

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

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

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

575575 | Just d <- lookup e path

576576 = if desc > 0

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

587587 -- rest definitely terminates without

588588 -- any cycles with route so far,

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

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

592592 Total _ -> return Unchecked

593593 x -> return x

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

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

608608 | otherwise = Unchecked

609609

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

611+

610612collapseNothing ((Nothing, _) : xs)

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

612614 Nothing -> False

src/Idris/ElabTerm.hs+1−2

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

477477 where elabArg n t

478478 = do hs <- get_holes

479479 tm <- get_term

480− t' <- insertCoerce ina t

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

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

483482 case n `elem` hs of

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

485484-- if r

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

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

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

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

489488 False -> return failed

490489 elabArgs ina failed fc r ns args

491490

src/Idris/Parser.hs+1

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

213213closeBlock :: IParser ()

214214closeBlock = do ist <- getState

215215 bs <- case brace_stack ist of

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

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

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

218219 inp <- getInput