29a1e77 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master'

29a1e77David Raymond Christiansen13 years ago

CHANGELOG+12−9

compare with master

unifiedsplit

@@ -4,18 +4,21 @@ New in 0.9.12:

4* Proof search now works for metavariables in types, giving some interactive

5 type inference.

6* New 'Lazy' type, replacing laziness annotations.

7−* JavaScript and Node codegen now understand the %include directive

7+* JavaScript and Node codegen now understand the %include directive.

8−* Concept up 'null' is now understood in the JavaScript and Node codegen

8+* Concept up 'null' is now understood in the JavaScript and Node codegen.

9−* Lots of performance patches for generated JavaScript

9+* Lots of performance patches for generated JavaScript.

10* New commands :eval (:e) and :type (:t) in the prover, which either normalise

11− or show the type of expressions

11+ or show the type of expressions.

12−* Allow type providers to return postulates in addition to terms

12+* Allow type providers to return postulates in addition to terms.

13+* Syntax for dealing with match failure in <- and pattern matching let.

13* New syntax for inline documentation. Documentation starts with |||, and

14* New syntax for inline documentation. Documentation starts with |||, and

14 arguments are documented by preceding their name with @. Example:

15 arguments are documented by preceding their name with @. Example:

15−||| Add two natural numbers

16+ ||| Add two natural numbers

16−||| @ n the first number (examined by the function)

17+ ||| @ n the first number (examined by the function)

17−||| @ m the second number (not examined)

18+ ||| @ m the second number (not examined)

18−plus (n, m : Nat) -> Nat

19+ plus (n, m : Nat) -> Nat

20+* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

21+ of proof automation. Use ":set autosolve" and ":unset autosolve".

20New in 0.9.11:

23New in 0.9.11:

21--------------

24--------------

Makefile+1−1

@@ -39,7 +39,7 @@ relib: lib_clean

39 $(CABAL) install $(CABALFLAGS)

41linecount:

42− wc -l src/Idris/*.hs src/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

42+ wc -l src/Idris/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

44#Note: this doesn't yet link to Hackage properly

45doc: dist/setup-config

idris.cabal+2

@@ -440,6 +440,7 @@ Library

440 , Idris.DeepSeq

441 , Idris.Delaborate

442 , Idris.Docs

443+ , Idris.Docstrings

443 , Idris.ElabDecls

444 , Idris.ElabDecls

444 , Idris.ElabTerm

445 , Idris.ElabTerm

445 , Idris.Error

446 , Idris.Error

@@ -506,6 +507,7 @@ Library

506 , ansi-wl-pprint

507 , ansi-wl-pprint

507 , binary

508 , binary

508 , bytestring

509 , bytestring

510+ , cheapskate

509 , containers >= 0.5

511 , containers >= 0.5

510 , directory

512 , directory

511 , directory >= 1.2

513 , directory >= 1.2

libs/neweffects/Effects.idr+7−2

@@ -171,7 +171,7 @@ data Eff : (m : Type -> Type) ->

171

172 lift : (prf : SubList ys xs) ->

173 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

174− new : Handler e m =>

174+ newInit : Handler e m =>

175 res ->

176 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

177 Eff m a xs (\v => xs')

@@ -226,7 +226,7 @@ eff env (effect prf effP) k = execEff env prf effP k

226eff env (lift prf effP) k

227 = let env' = dropEnv env prf in

228 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

229−eff env (new r prog) k

229+eff env (newInit r prog) k

230 = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)

231eff env (catch prog handler) k

232 = catch (eff env prog k)

@@ -265,6 +265,11 @@ effect' : {a, b: _} -> {e : Effect} ->

265 Eff m t xs (\v => updateResTy v xs prf eff)

266effect' e {prf} = effect prf e

267

268+new : Handler e m =>

269+ {default default r : res} ->

270+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

271+ Eff m a xs (\v => xs')

272+new {r} e = newInit r e

268

273

269run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

274run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

270run {env} prog = eff env prog (\r, env => pure r)

275run {env} prog = eff env prog (\r, env => pure r)

src/IRTS/CodegenJavaScript.hs+7−4

@@ -100,18 +100,18 @@ data FFI = FFICode Char | FFIArg Int | FFIError String

100ffi :: String -> [String] -> String

101ffi code args = let parsed = ffiParse code in

102 case ffiError parsed of

103− Just err -> compileJS $ jsError err

103+ Just err -> error err

104 Nothing -> renderFFI parsed args

105 where

106 ffiParse :: String -> [FFI]

107 ffiParse "" = []

108− ffiParse ['%'] = [FFIError "Invalid positional argument"]

108+ ffiParse ['%'] = [FFIError $ "FFI - Invalid positional argument"]

109 ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss

110 ffiParse ('%':s:ss)

111 | isDigit s =

112 FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)

113 | otherwise =

114− [FFIError "Invalid positional argument"]

114+ [FFIError $ "FFI - Invalid positional argument"]

115 ffiParse (s:ss) = FFICode s : ffiParse ss

116

117

@@ -126,7 +126,7 @@ ffi code args = let parsed = ffiParse code in

126 renderFFI ((FFICode c) : fs) args = c : renderFFI fs args

127 renderFFI ((FFIArg i) : fs) args

128 | i < length args && i >= 0 = args !! i ++ renderFFI fs args

129− | otherwise = "Argument index out of bounds"

129+ | otherwise = error "FFI - Argument index out of bounds"

130

131

132compileJS :: JS -> String

@@ -1964,6 +1964,9 @@ translateExpression (SForeign _ _ "isNull" [(FPtr, var)]) =

1964translateExpression (SForeign _ _ "idris_eqPtr" [(FPtr, lhs),(FPtr, rhs)]) =

1965 JSBinOp "==" (JSVar lhs) (JSVar rhs)

1966

1967+translateExpression (SForeign _ _ "idris_time" []) =

1968+ JSRaw "(new Date()).getTime()"

1969+

1967translateExpression (SForeign _ _ fun args) =

1970translateExpression (SForeign _ _ fun args) =

1968 JSFFI fun (map generateWrapper args)

1971 JSFFI fun (map generateWrapper args)

1969 where

1972 where

src/Idris/AbsSyntax.hs+8−1

@@ -9,6 +9,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))

9import Idris.Core.Typecheck

10import Idris.AbsSyntaxTree

11import Idris.Colours

12+import Idris.Docstrings

12import Idris.IdeSlave

13import Idris.IdeSlave

13import IRTS.CodegenCommon

14import IRTS.CodegenCommon

14import Util.DynamicLinker

15import Util.DynamicLinker

@@ -262,7 +263,7 @@ addCoercion :: Name -> Idris ()

262addCoercion n = do i <- getIState

263addCoercion n = do i <- getIState

263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264

265

265−addDocStr :: Name -> String -> [(Name, String)] -> Idris ()

266+addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()

266addDocStr n doc args

267addDocStr n doc args

267 = do i <- getIState

268 = do i <- getIState

268 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

269 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

@@ -713,6 +714,12 @@ setShowOrigErr b = do i <- getIState

713 let opt' = opts { opt_origerr = b }

714 let opt' = opts { opt_origerr = b }

714 putIState $ i { idris_options = opt' }

715 putIState $ i { idris_options = opt' }

715

716

717+setAutoSolve :: Bool -> Idris ()

718+setAutoSolve b = do i <- getIState

719+ let opts = idris_options i

720+ let opt' = opts { opt_autoSolve = b }

721+ putIState $ i { idris_options = opt' }

722+

716setNoBanner :: Bool -> Idris ()

723setNoBanner :: Bool -> Idris ()

717setNoBanner n = do i <- getIState

724setNoBanner n = do i <- getIState

718 let opts = idris_options i

725 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+33−29

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

7import Idris.Core.Evaluate

8import Idris.Core.Elaborate hiding (Tactic(..))

9import Idris.Core.Typecheck

10+import Idris.Docstrings

10import IRTS.Lang

11import IRTS.Lang

11import IRTS.CodegenCommon

12import IRTS.CodegenCommon

12import Util.Pretty

13import Util.Pretty

@@ -53,7 +54,8 @@ data IOption = IOption { opt_logLevel :: Int,

53 opt_cpu :: String,

54 opt_cpu :: String,

54 opt_optLevel :: Word,

55 opt_optLevel :: Word,

55 opt_cmdline :: [Opt], -- remember whole command line

56 opt_cmdline :: [Opt], -- remember whole command line

56− opt_origerr :: Bool

57+ opt_origerr :: Bool,

58+ opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover

57 }

59 }

58 deriving (Show, Eq)

60 deriving (Show, Eq)

@@ -76,6 +78,7 @@ defaultOpts = IOption { opt_logLevel = 0

76 , opt_optLevel = 2

78 , opt_optLevel = 2

77 , opt_cmdline = []

79 , opt_cmdline = []

78 , opt_origerr = False

80 , opt_origerr = False

81+ , opt_autoSolve = True

79 }

82 }

81data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

84data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

@@ -111,7 +114,7 @@ data IState = IState {

111 idris_flags :: Ctxt [FnOpt],

114 idris_flags :: Ctxt [FnOpt],

112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

115 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_calledgraph :: Ctxt [Name],

116 idris_calledgraph :: Ctxt [Name],

114− idris_docstrings :: Ctxt (String, [(Name, String)]),

117+ idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),

115 idris_tyinfodata :: Ctxt TIData,

118 idris_tyinfodata :: Ctxt TIData,

116 idris_totcheck :: [(FC, Name)], -- names to check totality on

119 idris_totcheck :: [(FC, Name)], -- names to check totality on

117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

120 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

@@ -336,6 +339,7 @@ data Opt = Filename String

336 | Client String

339 | Client String

337 | ShowOrigErr

340 | ShowOrigErr

338 | AutoWidth -- ^ Automatically adjust terminal width

341 | AutoWidth -- ^ Automatically adjust terminal width

342+ | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

339 deriving (Show, Eq)

343 deriving (Show, Eq)

340

344

341-- Parsed declarations

345-- Parsed declarations

@@ -450,15 +454,15 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms

450-- datatypes and typeclasses.

454-- datatypes and typeclasses.

451data PDecl' t

455data PDecl' t

452 = PFix FC Fixity [String] -- ^ Fixity declaration

456 = PFix FC Fixity [String] -- ^ Fixity declaration

453− | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

457+ | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

454− | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

458+ | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate

455 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

459 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

456 | PCAF FC Name t -- ^ Top level constant

460 | PCAF FC Name t -- ^ Top level constant

457− | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

461+ | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

458 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

462 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

459 | PNamespace String [PDecl' t] -- ^ New namespace

463 | PNamespace String [PDecl' t] -- ^ New namespace

460− | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

464+ | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration

461− | PClass String SyntaxInfo FC

465+ | PClass Docstring SyntaxInfo FC

462 [t] -- constraints

466 [t] -- constraints

463 Name

467 Name

464 [(Name, t)] -- parameters

468 [(Name, t)] -- parameters

@@ -512,7 +516,7 @@ deriving instance NFData PClause'

512-- | Data declaration

516-- | Data declaration

513data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

517data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

514 d_tcon :: t, -- ^ Type constructor

518 d_tcon :: t, -- ^ Type constructor

515− d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors

519+ d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors

516 }

520 }

517 -- ^ Data declaration

521 -- ^ Data declaration

518 | PLaterdecl { d_name :: Name, d_tcon :: t }

522 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -737,7 +741,7 @@ type PTactic = PTactic' PTerm

737

741

738data PDo' t = DoExp FC t

742data PDo' t = DoExp FC t

739 | DoBind FC Name t

743 | DoBind FC Name t

740− | DoBindP FC t t

744+ | DoBindP FC t t [(t,t)]

741 | DoLet FC Name t t

745 | DoLet FC Name t t

742 | DoLetP FC t t

746 | DoLetP FC t t

743 deriving (Eq, Functor)

747 deriving (Eq, Functor)

@@ -749,7 +753,7 @@ deriving instance NFData PDo'

749instance Sized a => Sized (PDo' a) where

753instance Sized a => Sized (PDo' a) where

750 size (DoExp fc t) = 1 + size fc + size t

754 size (DoExp fc t) = 1 + size fc + size t

751 size (DoBind fc nm t) = 1 + size fc + size nm + size t

755 size (DoBind fc nm t) = 1 + size fc + size nm + size t

752− size (DoBindP fc l r) = 1 + size fc + size l + size r

756+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

753 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r

757 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r

754 size (DoLetP fc l r) = 1 + size fc + size l + size r

758 size (DoLetP fc l r) = 1 + size fc + size l + size r

755

759

@@ -948,9 +952,9 @@ inferTy = sMN 0 "__Infer"

948inferCon = sMN 0 "__infer"

952inferCon = sMN 0 "__infer"

949inferDecl = PDatadecl inferTy

953inferDecl = PDatadecl inferTy

950 PType

954 PType

951− [("", [], inferCon, PPi impl (sMN 0 "iType") PType (

955+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (

952− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

956+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

953− (PRef bi inferTy)), bi, [])]

957+ (PRef bi inferTy)), bi, [])]

954inferOpts = []

958inferOpts = []

955

959

956infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

960infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -978,7 +982,7 @@ primNames = [unitTy, unitCon,

978unitTy = sMN 0 "__Unit"

982unitTy = sMN 0 "__Unit"

979unitCon = sMN 0 "__II"

983unitCon = sMN 0 "__II"

980unitDecl = PDatadecl unitTy PType

984unitDecl = PDatadecl unitTy PType

981− [("", [], unitCon, PRef bi unitTy, bi, [])]

985+ [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]

982unitOpts = [DefaultEliminator]

986unitOpts = [DefaultEliminator]

983

987

984falseTy = sMN 0 "__False"

988falseTy = sMN 0 "__False"

@@ -988,12 +992,12 @@ falseOpts = []

988pairTy = sMN 0 "__Pair"

992pairTy = sMN 0 "__Pair"

989pairCon = sMN 0 "__MkPair"

993pairCon = sMN 0 "__MkPair"

990pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

994pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

991− [("", [], pairCon, PPi impl (n "A") PType (

995+ [(emptyDocstring, [], pairCon, PPi impl (n "A") PType (

992− PPi impl (n "B") PType (

996+ PPi impl (n "B") PType (

993− PPi expl (n "a") (PRef bi (n "A")) (

997+ PPi expl (n "a") (PRef bi (n "A")) (

994− PPi expl (n "b") (PRef bi (n "B"))

998+ PPi expl (n "b") (PRef bi (n "B"))

995− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

999+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

996− pexp (PRef bi (n "B"))])))), bi, [])]

1000+ pexp (PRef bi (n "B"))])))), bi, [])]

997 where n a = sMN 0 a

1001 where n a = sMN 0 a

998pairOpts = []

1002pairOpts = []

999

1003

@@ -1002,21 +1006,21 @@ eqCon = sUN "refl"

1002eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1006eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1003 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1007 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1004 PType)

1008 PType)

1005− [("", [], eqCon, PPi impl (n "A") PType (

1009+ [(emptyDocstring, [], eqCon, PPi impl (n "A") PType (

1006− PPi impl (n "x") (PRef bi (n "A"))

1010+ PPi impl (n "x") (PRef bi (n "A"))

1007− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1011+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1008− pimp (n "B") Placeholder False,

1012+ pimp (n "B") Placeholder False,

1009− pexp (PRef bi (n "x")),

1013+ pexp (PRef bi (n "x")),

1010− pexp (PRef bi (n "x"))])), bi, [])]

1014+ pexp (PRef bi (n "x"))])), bi, [])]

1011 where n a = sMN 0 a

1015 where n a = sMN 0 a

1012eqOpts = []

1016eqOpts = []

1013

1017

1014elimName = sUN "__Elim"

1018elimName = sUN "__Elim"

1015elimMethElimTy = sUN "__elimTy"

1019elimMethElimTy = sUN "__elimTy"

1016elimMethElim = sUN "elim"

1020elimMethElim = sUN "elim"

1017−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1021+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1018− [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1022+ [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1019− PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1023+ PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1020

1024

1021-- Defined in builtins.idr

1025-- Defined in builtins.idr

1022sigmaTy = sUN "Exists"

1026sigmaTy = sUN "Exists"

src/Idris/Completion.hs+5−1

@@ -108,7 +108,11 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

108

109completeOption :: CompletionFunc Idris

110completeOption = completeWord Nothing " \t" completeOpt

111− where completeOpt = return . completeWith ["errorcontext", "showimplicits", "originalerrors"]

111+ where completeOpt = return . completeWith [ "errorcontext"

112+ , "showimplicits"

113+ , "originalerrors"

114+ , "autosolve"

115+ ]

112

116

113completeConsoleWidth :: CompletionFunc Idris

117completeConsoleWidth :: CompletionFunc Idris

114completeConsoleWidth = completeWord Nothing " \t" completeW

118completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/DSL.hs+2−2

@@ -57,10 +57,10 @@ expandDo dsl (PDoBlock ds)

57 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

58 block b (DoBind fc n tm : rest)

59 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

60− block b (DoBindP fc p tm : rest)

60+ block b (DoBindP fc p tm alts : rest)

61 = PApp fc b [pexp tm, pexp (PLam (sMN 0 "bpat") Placeholder

62 (PCase fc (PRef fc (sMN 0 "bpat"))

63− [(p, block b rest)]))]

63+ ((p, block b rest) : alts)))]

64 block b (DoLet fc n ty tm : rest)

65 = PLet n ty tm (block b rest)

66 block b (DoLetP fc p tm : rest)

src/Idris/DeepSeq.hs+43−1

@@ -6,6 +6,48 @@ import Idris.AbsSyntaxTree

7import Control.DeepSeq

9+import qualified Cheapskate.Types as CT

10+

11+-- Manual from imported libs

12+instance NFData CT.Doc where

13+ rnf (CT.Doc opts contents) = rnf opts `seq` rnf contents `seq` ()

14+

15+instance NFData CT.Options where

16+ rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

17+

18+instance NFData CT.Block where

19+ rnf (CT.Para lines) = rnf lines `seq` ()

20+ rnf (CT.Header i lines) = rnf i `seq` rnf lines `seq` ()

21+ rnf (CT.Blockquote bs) = rnf bs `seq` ()

22+ rnf (CT.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()

23+ rnf (CT.CodeBlock attr txt) = rnf attr `seq` rnf txt `seq` ()

24+ rnf (CT.HtmlBlock txt) = rnf txt `seq` ()

25+ rnf CT.HRule = ()

26+

27+instance NFData CT.Inline where

28+ rnf (CT.Str txt) = rnf txt `seq` ()

29+ rnf CT.Space = ()

30+ rnf CT.SoftBreak = ()

31+ rnf CT.LineBreak = ()

32+ rnf (CT.Emph xs) = rnf xs `seq` ()

33+ rnf (CT.Strong xs) = rnf xs `seq` ()

34+ rnf (CT.Code xs) = rnf xs `seq` ()

35+ rnf (CT.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()

36+ rnf (CT.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()

37+ rnf (CT.Entity a) = rnf a `seq` ()

38+ rnf (CT.RawHtml x) = rnf x `seq` ()

39+

40+instance NFData CT.ListType where

41+ rnf (CT.Bullet c) = rnf c `seq` ()

42+ rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()

43+

44+instance NFData CT.CodeAttr where

45+ rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()

46+

47+instance NFData CT.NumWrapper where

48+ rnf CT.PeriodFollowing = ()

49+ rnf CT.ParenFollowing = ()

50+

9-- All generated by 'derive'

51-- All generated by 'derive'

11instance NFData Forceability where

53instance NFData Forceability where

@@ -226,7 +268,7 @@ instance (NFData t) => NFData (PTactic' t) where

226instance (NFData t) => NFData (PDo' t) where

268instance (NFData t) => NFData (PDo' t) where

227 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

269 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

228 rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

270 rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

229− rnf (DoBindP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

271+ rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

230 rnf (DoLet x1 x2 x3 x4)

272 rnf (DoLet x1 x2 x3 x4)

231 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

273 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

232 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

274 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

src/Idris/Docs.hs+15−13

@@ -1,3 +1,4 @@

1+{-# LANGUAGE PatternGuards #-}

1module Idris.Docs where

2module Idris.Docs where

3import Idris.AbsSyntax

4import Idris.AbsSyntax

@@ -5,6 +6,7 @@ import Idris.AbsSyntaxTree

5import Idris.Delaborate

6import Idris.Delaborate

6import Idris.Core.TT

7import Idris.Core.TT

7import Idris.Core.Evaluate

8import Idris.Core.Evaluate

9+import Idris.Docstrings

9import Util.Pretty

11import Util.Pretty

@@ -13,8 +15,8 @@ import Data.List

14-- TODO: Only include names with public/abstract accessibility

16-- TODO: Only include names with public/abstract accessibility

16−data FunDoc = FD Name String

18+data FunDoc = FD Name Docstring

17− [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs

19+ [(Name, PTerm, Plicity, Maybe Docstring)] -- args: name, ty, implicit, docs

18 PTerm -- function type

20 PTerm -- function type

19 (Maybe Fixity)

21 (Maybe Fixity)

20 deriving Show

22 deriving Show

@@ -22,16 +24,16 @@ data FunDoc = FD Name String

22data Docs = FunDoc FunDoc

24data Docs = FunDoc FunDoc

23 | DataDoc FunDoc -- type constructor docs

25 | DataDoc FunDoc -- type constructor docs

24 [FunDoc] -- data constructor docs

26 [FunDoc] -- data constructor docs

25− | ClassDoc Name String -- class docs

27+ | ClassDoc Name Docstring -- class docs

26 [FunDoc] -- method docs

28 [FunDoc] -- method docs

27 deriving Show

29 deriving Show

29−showDoc "" = empty

31+showDoc d | nullDocstring d = empty

30−showDoc x = text " -- " <> text x

32+ | otherwise = text " -- " <> renderDocstring d

32pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

34pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

33pprintFD imp (FD n doc args ty f)

35pprintFD imp (FD n doc args ty f)

34− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

36+ = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>

35 maybe empty (\f -> text (show f) <> line) f <>

37 maybe empty (\f -> text (show f) <> line) f <>

36 let argshow = showArgs args [] in

38 let argshow = showArgs args [] in

37 if not (null argshow)

39 if not (null argshow)

@@ -41,20 +43,20 @@ pprintFD imp (FD n doc args ty f)

41 where showArgs ((n, ty, Exp {}, d):args) bnd

43 where showArgs ((n, ty, Exp {}, d):args) bnd

42 = bindingOf n False <+> colon <+>

44 = bindingOf n False <+> colon <+>

43 pprintPTerm imp bnd ty <>

45 pprintPTerm imp bnd ty <>

44− showDoc (maybe "" id d) <> line

46+ showDoc (maybe emptyDocstring id d) <> line

45 :

47 :

46 showArgs args ((n, False):bnd)

48 showArgs args ((n, False):bnd)

47 showArgs ((n, ty, Constraint {}, d):args) bnd

49 showArgs ((n, ty, Constraint {}, d):args) bnd

48 = text "Class constraint" <+>

50 = text "Class constraint" <+>

49− pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line

51+ pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line

50 :

52 :

51 showArgs args ((n, True):bnd)

53 showArgs args ((n, True):bnd)

52 showArgs ((n, ty, Imp {}, d):args) bnd

54 showArgs ((n, ty, Imp {}, d):args) bnd

53− | not (null doc)

55+ | Just d' <- d

54 = text "(implicit)" <+>

56 = text "(implicit)" <+>

55 bindingOf n True <+> colon <+>

57 bindingOf n True <+> colon <+>

56 pprintPTerm imp bnd ty <>

58 pprintPTerm imp bnd ty <>

57− showDoc (maybe "" id d) <> line

59+ showDoc d' <> line

58 :

60 :

59 showArgs args ((n, True):bnd)

61 showArgs args ((n, True):bnd)

60 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

62 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

@@ -93,7 +95,7 @@ docClass n ci

93 = do i <- getIState

95 = do i <- getIState

94 let docstr = case lookupCtxt n (idris_docstrings i) of

96 let docstr = case lookupCtxt n (idris_docstrings i) of

95 [str] -> fst str

97 [str] -> fst str

96− _ -> ""

98+ _ -> emptyDocstring

97 mdocs <- mapM docFun (map fst (class_methods ci))

99 mdocs <- mapM docFun (map fst (class_methods ci))

98 return (ClassDoc n docstr mdocs)

100 return (ClassDoc n docstr mdocs)

101

@@ -102,7 +104,7 @@ docFun n

102 = do i <- getIState

104 = do i <- getIState

103 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

105 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

104 [d] -> d

106 [d] -> d

105− _ -> ("", [])

107+ _ -> noDocs

106 let ty = delabTy i n

108 let ty = delabTy i n

107 let args = getPArgNames ty argDocs

109 let args = getPArgNames ty argDocs

108 let infixes = idris_infixes i

110 let infixes = idris_infixes i

@@ -116,7 +118,7 @@ docFun n

116 funName (UN n) = str n

118 funName (UN n) = str n

117 funName (NS n _) = funName n

119 funName (NS n _) = funName n

118

120

119−getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]

121+getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]

120getPArgNames (PPi plicity name ty body) ds =

122getPArgNames (PPi plicity name ty body) ds =

121 (name, ty, plicity, lookup name ds) : getPArgNames body ds

123 (name, ty, plicity, lookup name ds) : getPArgNames body ds

122getPArgNames _ _ = []

124getPArgNames _ _ = []

src/Idris/Docstrings.hsnew file+80

@@ -0,0 +1,80 @@

1+-- | Wrapper around Markdown library

2+module Idris.Docstrings (

3+ Docstring, parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs

4+ ) where

6+import qualified Cheapskate as C

7+import qualified Cheapskate.Types as CT

9+import Util.Pretty

10+

11+import Idris.Core.TT (OutputAnnotation, Name)

12+

13+import qualified Data.Text as T

14+import qualified Data.Foldable as F

15+import qualified Data.Sequence as S

16+

17+type Docstring = CT.Doc

18+

19+parseDocstring :: T.Text -> CT.Doc

20+parseDocstring = C.markdown options

21+

22+

23+options = CT.Options { CT.sanitize = True

24+ , CT.allowRawHtml = False

25+ , CT.preserveHardBreaks = True

26+ , CT.debug = False

27+ }

28+

29+renderDocstring :: Docstring -> Doc OutputAnnotation

30+renderDocstring (CT.Doc _ blocks) = renderBlocks blocks

31+

32+renderBlocks :: CT.Blocks -> Doc OutputAnnotation

33+renderBlocks blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

34+ fmap renderBlock blocks

35+ | S.length blocks == 1 = renderBlock (S.index blocks 0)

36+ | otherwise = empty

37+

38+renderBlock :: CT.Block -> Doc OutputAnnotation

39+renderBlock (CT.Para inlines) = renderInlines inlines

40+renderBlock (CT.Header lvl inlines) = renderInlines inlines <+> parens (text (show lvl))

41+renderBlock (CT.Blockquote blocks) = indent 8 $ renderBlocks blocks

42+renderBlock (CT.List b ty blockss) = renderList b ty blockss

43+renderBlock (CT.CodeBlock attr src) = indent 8 $ text (T.unpack src)

44+renderBlock (CT.HtmlBlock txt) = text "<html block>" -- TODO

45+renderBlock CT.HRule = text "----------------------"

46+

47+renderList :: Bool -> CT.ListType -> [CT.Blocks] -> Doc OutputAnnotation

48+renderList b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks) blockss

49+renderList b (CT.Numbered nw i) blockss =

50+ vsep $

51+ zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

52+ [i..] (repeat punc) (map renderBlocks blockss)

53+ where punc = case nw of

54+ CT.PeriodFollowing -> char '.'

55+ CT.ParenFollowing -> char '('

56+

57+renderInlines :: CT.Inlines -> Doc OutputAnnotation

58+renderInlines = F.foldr (<>) empty . fmap renderInline

59+

60+renderInline :: CT.Inline -> Doc OutputAnnotation

61+renderInline (CT.Str s) = text $ T.unpack s

62+renderInline CT.Space = space

63+renderInline CT.SoftBreak = softline

64+renderInline CT.LineBreak = line

65+renderInline (CT.Emph txt) = renderInlines txt -- TODO

66+renderInline (CT.Strong txt) = renderInlines txt -- TODO

67+renderInline (CT.Code txt) = text $ T.unpack txt

68+renderInline (CT.Link body url title) = renderInlines body <+> parens (text $ T.unpack url)

69+renderInline (CT.Image body url title) = text "<image>" -- TODO

70+renderInline (CT.Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO

71+renderInline (CT.RawHtml txt) = text "<html content>" --TODO

72+

73+emptyDocstring :: Docstring

74+emptyDocstring = CT.Doc options S.empty

75+

76+nullDocstring :: Docstring -> Bool

77+nullDocstring (CT.Doc _ blocks) = S.null blocks

78+

79+noDocs :: (Docstring, [(Name, Docstring)])

80+noDocs = (emptyDocstring, [])

src/Idris/ElabDecls.hs+30−27

@@ -26,6 +26,8 @@ import Idris.Core.Execute

26import Idris.Core.Typecheck

27import Idris.Core.CaseTree

29+import Idris.Docstrings

30+

29import Control.DeepSeq

31import Control.DeepSeq

30import Control.Monad

32import Control.Monad

31import Control.Monad.State.Strict as State

33import Control.Monad.State.Strict as State

@@ -63,12 +65,12 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

63-- return (n, (i, top, t'))) ns

65-- return (n, (i, top, t'))) ns

65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

67-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

66−elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

68+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

67 FC -> FnOpts -> Name -> PTerm -> Idris Type

69 FC -> FnOpts -> Name -> PTerm -> Idris Type

68elabType = elabType' False

70elabType = elabType' False

70elabType' :: Bool -> -- normalise it

72elabType' :: Bool -> -- normalise it

71− ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

73+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

72 FC -> FnOpts -> Name -> PTerm -> Idris Type

74 FC -> FnOpts -> Name -> PTerm -> Idris Type

73elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

75elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

74 n = liftname info n_in in -}

76 n = liftname info n_in in -}

@@ -171,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

171 tyIsHandler _ = False

173 tyIsHandler _ = False

172

174

173

175

174−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

176+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

175 FC -> FnOpts -> Name -> PTerm -> Idris ()

177 FC -> FnOpts -> Name -> PTerm -> Idris ()

176elabPostulate info syn doc fc opts n ty

178elabPostulate info syn doc fc opts n ty

177 = do elabType info syn doc [] fc opts n ty

179 = do elabType info syn doc [] fc opts n ty

@@ -195,7 +197,7 @@ elabPostulate info syn doc fc opts n ty

195 -- remove it from the deferred definitions list

197 -- remove it from the deferred definitions list

196 solveDeferred n

198 solveDeferred n

197

199

198−elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()

200+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()

199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

201elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

200 = do let codata = Codata `elem` opts

202 = do let codata = Codata `elem` opts

201 iLOG (show (fc, doc))

203 iLOG (show (fc, doc))

@@ -257,8 +259,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

257 updateContext (addDatatype (Data n ttag cty cons))

259 updateContext (addDatatype (Data n ttag cty cons))

258 updateContext (setMetaInformation n metainf)

260 updateContext (setMetaInformation n metainf)

259 mapM_ (checkPositive n) cons

261 mapM_ (checkPositive n) cons

262+ if DefaultEliminator `elem` opts

260− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

263+ then evalStateT (elabEliminator params n t dcons info) Map.empty

261− else return ()

264+ else return ()

262 where

265 where

263 checkDefinedAs fc n t ctxt

266 checkDefinedAs fc n t ctxt

264 = case lookupDef n ctxt of

267 = case lookupDef n ctxt of

@@ -322,7 +325,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris

322

325

323-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

326-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

324elabEliminator :: [Int] -> Name -> PTerm ->

327elabEliminator :: [Int] -> Name -> PTerm ->

325− [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->

328+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

326 ElabInfo -> EliminatorState ()

329 ElabInfo -> EliminatorState ()

327elabEliminator paramPos n ty cons info = do

330elabEliminator paramPos n ty cons info = do

328 elimLog $ "Elaborating eliminator"

331 elimLog $ "Elaborating eliminator"

@@ -339,7 +342,7 @@ elabEliminator paramPos n ty cons info = do

339 let motiveConstr = [(motiveName, expl, motive)]

342 let motiveConstr = [(motiveName, expl, motive)]

340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

343 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

341 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

344 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

342− let eliminatorTyDecl = PTy (show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

345+ let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

343 let clauseConsElimArgs = map getPiName consTerms

346 let clauseConsElimArgs = map getPiName consTerms

344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

347 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

348 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -488,7 +491,7 @@ elabEliminator paramPos n ty cons info = do

488 splitArgPms _ = ([],[])

491 splitArgPms _ = ([],[])

489

492

490

493

491− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

494+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

492 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

495 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

493 i <- State.lift getIState

496 i <- State.lift getIState

494 implargs' <- case lookupCtxt cnm (idris_implicits i) of

497 implargs' <- case lookupCtxt cnm (idris_implicits i) of

@@ -503,7 +506,7 @@ elabEliminator paramPos n ty cons info = do

503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

506 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

504 _ -> return implargs

507 _ -> return implargs

505

508

506− extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

509+ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

507 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

510 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

508 let cons' = replaceParams paramPos generalParameters ty

511 let cons' = replaceParams paramPos generalParameters ty

509 let (args, resTy) = splitPi cons'

512 let (args, resTy) = splitPi cons'

@@ -539,7 +542,7 @@ elabEliminator paramPos n ty cons info = do

539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

542 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

540 convertImplPi _ = Nothing

543 convertImplPi _ = Nothing

541

544

542− generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

545+ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

543 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

546 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

544 let cons' = replaceParams paramPos generalParameters ty

547 let cons' = replaceParams paramPos generalParameters ty

545 let (args, resTy) = splitPi cons'

548 let (args, resTy) = splitPi cons'

@@ -561,7 +564,7 @@ elabEliminator paramPos n ty cons info = do

561

564

562elabPrims :: Idris ()

565elabPrims :: Idris ()

563elabPrims = do mapM_ (elabDecl EAll toplevel)

566elabPrims = do mapM_ (elabDecl EAll toplevel)

564− (map (\(opt, decl) -> PData "" [] defaultSyntax (fileFC "builtin") opt decl)

567+ (map (\(opt, decl) -> PData emptyDocstring [] defaultSyntax (fileFC "builtin") opt decl)

565 (zip

568 (zip

566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

569 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

570 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

@@ -665,7 +668,7 @@ elabProvider info syn fc what n ty tm

665 Provide tm

668 Provide tm

666 | what `elem` [ProvTerm, ProvAny] ->

669 | what `elem` [ProvTerm, ProvAny] ->

667 do -- Finally add a top-level definition of the provided term

670 do -- Finally add a top-level definition of the provided term

668− elabType info syn "" [] fc [] n ty

671+ elabType info syn emptyDocstring [] fc [] n ty

669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

672 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

670 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

673 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

671 | otherwise ->

674 | otherwise ->

@@ -673,7 +676,7 @@ elabProvider info syn fc what n ty tm

673 Postulate

676 Postulate

674 | what `elem` [ProvPostulate, ProvAny] ->

677 | what `elem` [ProvPostulate, ProvAny] ->

675 do -- Add the postulate

678 do -- Add the postulate

676− elabPostulate info syn "Provided postulate" fc [] n ty

679+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty

677 logLvl 3 $ "Elaborated provided postulate " ++ show n

680 logLvl 3 $ "Elaborated provided postulate " ++ show n

678 | otherwise ->

681 | otherwise ->

679 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

682 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

@@ -724,8 +727,8 @@ elabTransform info fc safe lhs_in rhs_in

724 addIBC (IBCTrans (clhs_tm, crhs_tm))

727 addIBC (IBCTrans (clhs_tm, crhs_tm))

725

728

726

729

727−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

730+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

728− PTerm -> String -> Name -> PTerm -> Idris ()

731+ PTerm -> Docstring -> Name -> PTerm -> Idris ()

729elabRecord info syn doc fc tyn ty cdoc cn cty

732elabRecord info syn doc fc tyn ty cdoc cn cty

730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

733 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

731 cty' <- implicit syn cn cty

734 cty' <- implicit syn cn cty

@@ -797,7 +800,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

797

800

798 mkProj recty substs cimp ((pn_in, pty), pos)

801 mkProj recty substs cimp ((pn_in, pty), pos)

799 = do let pn = expandNS syn pn_in

802 = do let pn = expandNS syn pn_in

800− let pfnTy = PTy "" [] defaultSyntax fc [] pn

803+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

801 (PPi expl rec recty

804 (PPi expl rec recty

802 (substMatches substs pty))

805 (substMatches substs pty))

803 let pls = repeat Placeholder

806 let pls = repeat Placeholder

@@ -818,7 +821,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

818 let valname = sMN 0 "updateval"

821 let valname = sMN 0 "updateval"

819 let pt = k (PPi expl pn pty

822 let pt = k (PPi expl pn pty

820 (PPi expl rec recty recty))

823 (PPi expl rec recty recty))

821− let pfnTy = PTy "" [] defaultSyntax fc [] setname pt

824+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt

822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

825 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

823 let lhsArgs = pls

826 let lhsArgs = pls

824 let rhsArgs = take pos pls ++ (PRef fc valname) :

827 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -834,7 +837,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

834 return (pn, pfnTy, PClauses fc [] setname [pclause])

837 return (pn, pfnTy, PClauses fc [] setname [pclause])

835

838

836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

839elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

837− (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

840+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

841elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

839 = do checkUndefined fc n

842 = do checkUndefined fc n

840 ctxt <- getContext

843 ctxt <- getContext

@@ -1166,7 +1169,7 @@ elabPE info fc caller r =

1166 (map (\ (lhs, rhs) ->

1169 (map (\ (lhs, rhs) ->

1167 (showTmImpls lhs ++ " = " ++

1170 (showTmImpls lhs ++ " = " ++

1168 showTmImpls rhs)) pats)

1171 showTmImpls rhs)) pats)

1169− elabType info defaultSyntax "" [] fc opts newnm specTy

1172+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

1170 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1173 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1171 elabClauses info fc opts newnm def

1174 elabClauses info fc opts newnm def

1172 logLvl 2 $ "Specialised " ++ show newnm)

1175 logLvl 2 $ "Specialised " ++ show newnm)

@@ -1725,7 +1728,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1725

1728

1726data MArgTy = IA | EA | CA deriving Show

1729data MArgTy = IA | EA | CA deriving Show

1727

1730

1728−elabClass :: ElabInfo -> SyntaxInfo -> String ->

1731+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

1729 FC -> [PTerm] ->

1732 FC -> [PTerm] ->

1730 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1733 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1731elabClass info syn doc fc constraints tn ps ds

1734elabClass info syn doc fc constraints tn ps ds

@@ -1752,7 +1755,7 @@ elabClass info syn doc fc constraints tn ps ds

1752 let cty = impbind ps $ conbind constraints

1755 let cty = impbind ps $ conbind constraints

1753 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1756 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1754 constraint

1757 constraint

1755− let cons = [("", [], cn, cty, fc, [])]

1758+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]

1756 let ddecl = PDatadecl tn tty cons

1759 let ddecl = PDatadecl tn tty cons

1757 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1760 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1758 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

1761 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

@@ -1807,7 +1810,7 @@ elabClass info syn doc fc constraints tn ps ds

1807 case lookup n mtys of

1810 case lookup n mtys of

1808 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1811 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1809 let ds = map (decorateid defaultdec)

1812 let ds = map (decorateid defaultdec)

1810− [PTy "" [] syn fc [] n ty',

1813+ [PTy emptyDocstring [] syn fc [] n ty',

1811 PClauses fc (o ++ opts) n cs]

1814 PClauses fc (o ++ opts) n cs]

1812 iLOG (show ds)

1815 iLOG (show ds)

1813 return (n, ((defaultdec n, ds!!1), ds))

1816 return (n, ((defaultdec n, ds!!1), ds))

@@ -1845,7 +1848,7 @@ elabClass info syn doc fc constraints tn ps ds

1845 addInstance False conn' cfn

1848 addInstance False conn' cfn

1846 addIBC (IBCInstance False conn' cfn)

1849 addIBC (IBCInstance False conn' cfn)

1847-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1850-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1848− return [PTy "" [] syn fc [] cfn ty,

1851+ return [PTy emptyDocstring [] syn fc [] cfn ty,

1849 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1852 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1850

1853

1851 -- Generate a top level function which looks up a method in a given

1854 -- Generate a top level function which looks up a method in a given

@@ -1909,7 +1912,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

1909 let constraint = PApp fc (PRef fc n) (map pexp ps)

1912 let constraint = PApp fc (PRef fc n) (map pexp ps)

1910 let iname = mkiname n ps expn

1913 let iname = mkiname n ps expn

1911 when (what /= EDefns) $ do

1914 when (what /= EDefns) $ do

1912− nty <- elabType' True info syn "" [] fc [] iname t

1915+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t

1913 -- if the instance type matches any of the instances we have already,

1916 -- if the instance type matches any of the instances we have already,

1914 -- and it's not a named instance, then it's overlapping, so report an error

1917 -- and it's not a named instance, then it's overlapping, so report an error

1915 case expn of

1918 case expn of

@@ -2061,7 +2064,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2061 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2064 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2062 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2063

2066

2064− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t

2067+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

2065

2068

2066 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2069 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2067 conbind [] x = x

2070 conbind [] x = x

@@ -2308,7 +2311,7 @@ inferredDiff fc inf user =

2308-- | Check a PTerm against documentation and ensure that every documented

2311-- | Check a PTerm against documentation and ensure that every documented

2309-- argument actually exists. This must be run _after_ implicits have been

2312-- argument actually exists. This must be run _after_ implicits have been

2310-- found, or it will give spurious errors.

2313-- found, or it will give spurious errors.

2311−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()

2314+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()

2312checkDocs fc args tm = cd (Map.fromList args) tm

2315checkDocs fc args tm = cd (Map.fromList args) tm

2313 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

2316 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

2314 cd as _ | Map.null as = return ()

2317 cd as _ | Map.null as = return ()

src/Idris/IBC.hs+93−8

@@ -9,6 +9,9 @@ import Idris.AbsSyntax

9import Idris.Imports

10import Idris.Error

11import Idris.Delaborate

12+import Idris.Docstrings

13+

14+import qualified Cheapskate.Types as CT

13import Data.Binary

16import Data.Binary

14import Data.Vector.Binary

17import Data.Vector.Binary

@@ -25,7 +28,7 @@ import Codec.Compression.Zlib (compress)

25import Util.Zlib (decompressEither)

28import Util.Zlib (decompressEither)

27ibcVersion :: Word8

30ibcVersion :: Word8

28−ibcVersion = 62

31+ibcVersion = 63

31data IBCFile = IBCFile { ver :: Word8,

34data IBCFile = IBCFile { ver :: Word8,

@@ -52,7 +55,7 @@ data IBCFile = IBCFile { ver :: Word8,

52 ibc_flags :: [(Name, [FnOpt])],

55 ibc_flags :: [(Name, [FnOpt])],

53 ibc_cg :: [(Name, CGInfo)],

56 ibc_cg :: [(Name, CGInfo)],

54 ibc_defs :: [(Name, Def)],

57 ibc_defs :: [(Name, Def)],

55− ibc_docstrings :: [(Name, (String, [(Name, String)]))],

58+ ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],

56 ibc_transforms :: [(Term, Term)],

59 ibc_transforms :: [(Term, Term)],

57 ibc_errRev :: [(Term, Term)],

60 ibc_errRev :: [(Term, Term)],

58 ibc_coercions :: [Name],

61 ibc_coercions :: [Name],

@@ -405,7 +408,7 @@ pDefs syms ds

405 update (Proj t i) = Proj (update t) i

408 update (Proj t i) = Proj (update t) i

406 update t = t

409 update t = t

407

410

408−pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()

411+pDocs :: [(Name, (Docstring, [(Name, Docstring)]))] -> Idris ()

409pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

412pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

410

413

411pAccess :: [(Name, Accessibility)] -> Idris ()

414pAccess :: [(Name, Accessibility)] -> Idris ()

@@ -461,6 +464,86 @@ pMetavars ns = do i <- getIState

461 putIState $ i { idris_metavars = Data.List.reverse ns

464 putIState $ i { idris_metavars = Data.List.reverse ns

462 ++ idris_metavars i }

465 ++ idris_metavars i }

463

466

467+----- For Cheapskate

468+

469+instance Binary CT.Doc where

470+ put (CT.Doc opts lines) = do put opts ; put lines

471+ get = do opts <- get

472+ lines <- get

473+ return (CT.Doc opts lines)

474+

475+instance Binary CT.Options where

476+ put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4

477+ get = do x1 <- get

478+ x2 <- get

479+ x3 <- get

480+ x4 <- get

481+ return (CT.Options x1 x2 x3 x4)

482+

483+instance Binary CT.Block where

484+ put (CT.Para lines) = do putWord8 0 ; put lines

485+ put (CT.Header i lines) = do putWord8 1 ; put i ; put lines

486+ put (CT.Blockquote bs) = do putWord8 2 ; put bs

487+ put (CT.List b t xs) = do putWord8 3 ; put b ; put t ; put xs

488+ put (CT.CodeBlock attr txt) = do putWord8 4 ; put attr ; put txt

489+ put (CT.HtmlBlock txt) = do putWord8 5 ; put txt

490+ put CT.HRule = putWord8 6

491+ get = do i <- getWord8

492+ case i of

493+ 0 -> fmap CT.Para get

494+ 1 -> liftM2 CT.Header get get

495+ 2 -> fmap CT.Blockquote get

496+ 3 -> liftM3 CT.List get get get

497+ 4 -> liftM2 CT.CodeBlock get get

498+ 5 -> liftM CT.HtmlBlock get

499+ 6 -> return CT.HRule

500+

501+instance Binary CT.Inline where

502+ put (CT.Str txt) = do putWord8 0 ; put txt

503+ put CT.Space = putWord8 1

504+ put CT.SoftBreak = putWord8 2

505+ put CT.LineBreak = putWord8 3

506+ put (CT.Emph xs) = putWord8 4 >> put xs

507+ put (CT.Strong xs) = putWord8 5 >> put xs

508+ put (CT.Code xs) = putWord8 6 >> put xs

509+ put (CT.Link a b c) = putWord8 7 >> put a >> put b >> put c

510+ put (CT.Image a b c) = putWord8 8 >> put a >> put b >> put c

511+ put (CT.Entity a) = putWord8 9 >> put a

512+ put (CT.RawHtml x) = putWord8 10 >> put x

513+ get = do i <- getWord8

514+ case i of

515+ 0 -> liftM CT.Str get

516+ 1 -> return CT.Space

517+ 2 -> return CT.SoftBreak

518+ 3 -> return CT.LineBreak

519+ 4 -> liftM CT.Emph get

520+ 5 -> liftM CT.Strong get

521+ 6 -> liftM CT.Code get

522+ 7 -> liftM3 CT.Link get get get

523+ 8 -> liftM3 CT.Image get get get

524+ 9 -> liftM CT.Entity get

525+ 10 -> liftM CT.RawHtml get

526+

527+instance Binary CT.ListType where

528+ put (CT.Bullet c) = putWord8 0 >> put c

529+ put (CT.Numbered nw i) = putWord8 1 >> put nw >> put i

530+ get = do i <- getWord8

531+ case i of

532+ 0 -> liftM CT.Bullet get

533+ 1 -> liftM2 CT.Numbered get get

534+

535+instance Binary CT.CodeAttr where

536+ put (CT.CodeAttr a b) = put a >> put b

537+ get = liftM2 CT.CodeAttr get get

538+

539+instance Binary CT.NumWrapper where

540+ put (CT.PeriodFollowing) = putWord8 0

541+ put (CT.ParenFollowing) = putWord8 1

542+ get = do i <- getWord8

543+ case i of

544+ 0 -> return CT.PeriodFollowing

545+ 1 -> return CT.ParenFollowing

546+

464----- Generated by 'derive'

547----- Generated by 'derive'

465

548

466instance Binary SizeChange where

549instance Binary SizeChange where

@@ -1878,10 +1961,11 @@ instance (Binary t) => Binary (PDo' t) where

1878 put x1

1961 put x1

1879 put x2

1962 put x2

1880 put x3

1963 put x3

1881− DoBindP x1 x2 x3 -> do putWord8 2

1964+ DoBindP x1 x2 x3 x4 -> do putWord8 2

1882− put x1

1965+ put x1

1883− put x2

1966+ put x2

1884− put x3

1967+ put x3

1968+ put x4

1885 DoLet x1 x2 x3 x4 -> do putWord8 3

1969 DoLet x1 x2 x3 x4 -> do putWord8 3

1886 put x1

1970 put x1

1887 put x2

1971 put x2

@@ -1904,7 +1988,8 @@ instance (Binary t) => Binary (PDo' t) where

1904 2 -> do x1 <- get

1988 2 -> do x1 <- get

1905 x2 <- get

1989 x2 <- get

1906 x3 <- get

1990 x3 <- get

1991+ x4 <- get

1907− return (DoBindP x1 x2 x3)

1992+ return (DoBindP x1 x2 x3 x4)

1908 3 -> do x1 <- get

1993 3 -> do x1 <- get

1909 x2 <- get

1994 x2 <- get

1910 x3 <- get

1995 x3 <- get

src/Idris/ParseData.hs+8−6

@@ -20,6 +20,8 @@ import Idris.DSL

20import Idris.Core.TT

21import Idris.Core.Evaluate

23+import Idris.Docstrings

24+

23import Control.Applicative

25import Control.Applicative

24import Control.Monad

26import Control.Monad

25import Control.Monad.State.Strict

27import Control.Monad.State.Strict

@@ -41,7 +43,7 @@ Record ::=

41-}

43-}

42record :: SyntaxInfo -> IdrisParser PDecl

44record :: SyntaxInfo -> IdrisParser PDecl

43record syn = do (doc, acc) <- try (do

45record syn = do (doc, acc) <- try (do

44− doc <- option ("", []) docComment

46+ doc <- option noDocs docComment

45 acc <- optional accessibility

47 acc <- optional accessibility

46 reserved "record"

48 reserved "record"

47 return (doc, acc))

49 return (doc, acc))

@@ -103,7 +105,7 @@ SimpleConstructorList ::=

103-}

105-}

104data_ :: SyntaxInfo -> IdrisParser PDecl

106data_ :: SyntaxInfo -> IdrisParser PDecl

105data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

107data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

106− (doc, argDocs) <- option ("", []) docComment

108+ (doc, argDocs) <- option noDocs docComment

107 pushIndent

109 pushIndent

108 acc <- optional accessibility

110 acc <- optional accessibility

109 elim <- dataOpts []

111 elim <- dataOpts []

@@ -160,9 +162,9 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

160{- | Parses a type constructor declaration

162{- | Parses a type constructor declaration

161 Constructor ::= DocComment? FnName TypeSig;

163 Constructor ::= DocComment? FnName TypeSig;

162-}

164-}

163−constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])

165+constructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])

164constructor syn

166constructor syn

165− = do (doc, argDocs) <- option ("", []) docComment

167+ = do (doc, argDocs) <- option noDocs docComment

166 cn_in <- fnName; fc <- getFC

168 cn_in <- fnName; fc <- getFC

167 let cn = expandNS syn cn_in

169 let cn = expandNS syn cn_in

168 lchar ':'

170 lchar ':'

@@ -177,9 +179,9 @@ constructor syn

177{- | Parses a constructor for simple discriminative union data types

179{- | Parses a constructor for simple discriminative union data types

178 SimpleConstructor ::= FnName SimpleExpr* DocComment?

180 SimpleConstructor ::= FnName SimpleExpr* DocComment?

179-}

181-}

180−simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])

182+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, [PTerm], FC, [Name])

181simpleConstructor syn

183simpleConstructor syn

182− = do doc <- option ("", []) (try docComment)

184+ = do doc <- option noDocs (try docComment)

183 cn_in <- fnName

185 cn_in <- fnName

184 let cn = expandNS syn cn_in

186 let cn = expandNS syn cn_in

185 fc <- getFC

187 fc <- getFC

src/Idris/ParseExpr.hs+25−6

@@ -167,7 +167,9 @@ extension syn (Rule ssym ptm _)

167 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds

168 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)

169 : upd (dropn n ns) ds

170+ upd ns (DoBindP fc i t ts : ds)

170− upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)

171+ = DoBindP fc (update ns i) (update ns t)

172+ (map (\(l,r) -> (update ns l, update ns r)) ts)

171 : upd ns ds

173 : upd ns ds

172 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)

174 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)

173 : upd ns ds

175 : upd ns ds

@@ -736,16 +738,22 @@ TypeSig' ::=

736@

738@

737 -}

739 -}

738let_ :: SyntaxInfo -> IdrisParser PTerm

740let_ :: SyntaxInfo -> IdrisParser PTerm

739−let_ syn = try (do reserved "let"; n <- name;

741+let_ syn = try (do reserved "let"; fc <- getFC; n <- name;

740 ty <- option Placeholder (do lchar ':'; expr' syn)

742 ty <- option Placeholder (do lchar ':'; expr' syn)

741 lchar '='

743 lchar '='

742 v <- expr syn

744 v <- expr syn

745+ ts <- option [] (do lchar '|'

746+ sepBy1 (do_alt syn) (lchar '|'))

743 reserved "in"; sc <- expr syn

747 reserved "in"; sc <- expr syn

748+ case ts of

744− return (PLet n ty v sc))

749+ [] -> return (PLet n ty v sc)

750+ alts -> return (PCase fc v ((PRef fc n, sc) : ts)))

745 <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

751 <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

746 symbol "="; v <- expr syn

752 symbol "="; v <- expr syn

753+ ts <- option [] (do lchar '|'

754+ sepBy1 (do_alt syn) (lchar '|'))

747 reserved "in"; sc <- expr syn

755 reserved "in"; sc <- expr syn

748− return (PCase fc v [(pat, sc)]))

756+ return (PCase fc v ((pat, sc) : ts)))

749 <?> "let binding"

757 <?> "let binding"

750

758

751{- | Parses a quote goal

759{- | Parses a quote goal

@@ -967,17 +975,28 @@ do_ syn

967 symbol "<-"

975 symbol "<-"

968 fc <- getFC

976 fc <- getFC

969 e <- expr syn;

977 e <- expr syn;

970− return (DoBind fc i e))

978+ option (DoBind fc i e)

979+ (do lchar '|'

980+ ts <- sepBy1 (do_alt syn) (lchar '|')

981+ return (DoBindP fc (PRef fc i) e ts)))

971 <|> try (do i <- expr' syn

982 <|> try (do i <- expr' syn

972 symbol "<-"

983 symbol "<-"

973 fc <- getFC

984 fc <- getFC

974 e <- expr syn;

985 e <- expr syn;

986+ option (DoBindP fc i e [])

987+ (do lchar '|'

988+ ts <- sepBy1 (do_alt syn) (lchar '|')

975− return (DoBindP fc i e))

989+ return (DoBindP fc i e ts)))

976 <|> do e <- expr syn

990 <|> do e <- expr syn

977 fc <- getFC

991 fc <- getFC

978 return (DoExp fc e)

992 return (DoExp fc e)

979 <?> "do block expression"

993 <?> "do block expression"

980

994

995+do_alt syn = do l <- expr' syn

996+ symbol "=>"

997+ r <- expr' syn

998+ return (l, r)

999+

981{- | Parses an expression in idiom brackets

1000{- | Parses an expression in idiom brackets

982@

1001@

983Idiom ::= '[|' Expr '|]';

1002Idiom ::= '[|' Expr '|]';

src/Idris/ParseHelpers.hs+14−9

@@ -1,4 +1,5 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2+{-# LANGUAGE StandaloneDeriving #-}

2module Idris.ParseHelpers where

3module Idris.ParseHelpers where

4import Prelude hiding (pi)

5import Prelude hiding (pi)

@@ -16,6 +17,7 @@ import Idris.AbsSyntax

16import Idris.Core.TT

17import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19import Idris.Delaborate (pprintErr)

20+import Idris.Docstrings

20import qualified Util.Pretty as Pretty (text)

22import qualified Util.Pretty as Pretty (text)

@@ -41,7 +43,9 @@ import Debug.Trace

41type IdrisParser = StateT IState IdrisInnerParser

43type IdrisParser = StateT IState IdrisInnerParser

43newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

45newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

44− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)

46+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing{-, Parsing-}, DeltaParsing, MarkParsing Delta, Monoid)

47+

48+deriving instance Parsing IdrisInnerParser

46instance TokenParsing IdrisInnerParser where

50instance TokenParsing IdrisInnerParser where

47 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

51 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

@@ -139,25 +143,26 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

139{-| Parses a documentation comment (similar to haddoc) given a marker character

143{-| Parses a documentation comment (similar to haddoc) given a marker character

140

144

141@

145@

142− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t

146+ DocComment_t ::= '|||' ~EOL_t* EOL_t

143− | '{ -' DocCommentMarket_t ~'- }'* '- }'

144 ;

147 ;

145@

148@

146 -}

149 -}

147−docComment :: IdrisParser (String, [(Name, String)])

150+docComment :: IdrisParser (Docstring, [(Name, Docstring)])

148docComment = do dc <- pushIndent *> docCommentLine

151docComment = do dc <- pushIndent *> docCommentLine

149 rest <- many (indented docCommentLine)

152 rest <- many (indented docCommentLine)

150 args <- many (indented argDocCommentLine)

153 args <- many (indented argDocCommentLine)

151 popIndent

154 popIndent

152− return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)

155+ return (parseDocstring $ T.pack (concat . intersperse "\n" $ dc:rest),

156+ map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

153

157

154 where docCommentLine :: MonadicParsing m => m String

158 where docCommentLine :: MonadicParsing m => m String

155 docCommentLine = try (do string "|||"

159 docCommentLine = try (do string "|||"

156− many (satisfy isSpace)

160+ many (satisfy (==' '))

157− first <- satisfy (\c -> not (isEol c || c == '@'))

161+ contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

158− res <- many (satisfy (not . isEol))

162+ res <- many (satisfy (not . isEol))

163+ return $ first:res)

159 eol ; someSpace

164 eol ; someSpace

160− return (first:res))-- ++ concat rest))

165+ return contents)-- ++ concat rest))

161 <?> ""

166 <?> ""

162 argDocCommentLine = do string "|||"

167 argDocCommentLine = do string "|||"

163 many (satisfy isSpace)

168 many (satisfy isSpace)

src/Idris/ParseOps.hs−1

@@ -59,7 +59,6 @@ binary name f = Infix (do fc <- getFC

59 indentPropHolds gtProp

60 reservedOp name

61 indentPropHolds gtProp

62− doc <- option ("", []) docComment

63 return (f fc))

62 return (f fc))

65-- | Prefix operator

64-- | Prefix operator

src/Idris/Parser.hs+7−5

@@ -35,6 +35,8 @@ import Idris.ParseOps

35import Idris.ParseExpr

36import Idris.ParseData

38+import Idris.Docstrings

39+

38import Paths_idris

40import Paths_idris

40import Util.DynamicLinker

42import Util.DynamicLinker

@@ -315,7 +317,7 @@ fnDecl' syn = checkFixity $

315 do (doc, fc, opts', n, acc) <- try (do

317 do (doc, fc, opts', n, acc) <- try (do

316 pushIndent

318 pushIndent

317 ist <- get

319 ist <- get

318− doc <- option ("", []) docComment

320+ doc <- option noDocs docComment

319 ist <- get

321 ist <- get

320 let initOpts = if default_total ist

322 let initOpts = if default_total ist

321 then [TotalFn]

323 then [TotalFn]

@@ -413,7 +415,7 @@ Postulate ::=

413@

415@

414-}

416-}

415postulate :: SyntaxInfo -> IdrisParser PDecl

417postulate :: SyntaxInfo -> IdrisParser PDecl

416−postulate syn = do doc <- try $ do doc <- option ("", []) docComment

418+postulate syn = do doc <- try $ do doc <- option noDocs docComment

417 pushIndent

419 pushIndent

418 reserved "postulate"

420 reserved "postulate"

419 return doc

421 return doc

@@ -561,7 +563,7 @@ Class ::=

561-}

563-}

562class_ :: SyntaxInfo -> IdrisParser [PDecl]

564class_ :: SyntaxInfo -> IdrisParser [PDecl]

563class_ syn = do (doc, acc) <- try (do

565class_ syn = do (doc, acc) <- try (do

564− doc <- option ("", []) docComment

566+ doc <- option noDocs docComment

565 acc <- optional accessibility

567 acc <- optional accessibility

566 return (doc, acc))

568 return (doc, acc))

567 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

569 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

@@ -1003,8 +1005,8 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1003 mapM_ (addNameHint ty') ns

1005 mapM_ (addNameHint ty') ns

1004 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

1006 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

1005 <|> do try (lchar '%' *> reserved "error_handlers")

1007 <|> do try (lchar '%' *> reserved "error_handlers")

1006− fn <- iName []

1008+ fn <- fnName

1007− arg <- iName []

1009+ arg <- fnName

1008 ns <- sepBy1 name (lchar ',')

1010 ns <- sepBy1 name (lchar ',')

1009 return [PDirective (do fn' <- disambiguate fn

1011 return [PDirective (do fn' <- disambiguate fn

1010 ns' <- mapM disambiguate ns

1012 ns' <- mapM disambiguate ns

src/Idris/Prover.hs+2−1

@@ -164,6 +164,7 @@ receiveInput e =

164ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165ploop fn d prompt prf e h

166 = do i <- getIState

167+ let autoSolve = opt_autoSolve (idris_options i)

167 when d $ dumpState i (proof e)

168 when d $ dumpState i (proof e)

168 (x, h') <-

169 (x, h') <-

169 case idris_outputmode i of

170 case idris_outputmode i of

@@ -260,7 +261,7 @@ ploop fn d prompt prf e h

260 return (False, e, False, prf))

261 return (False, e, False, prf))

261 (\err -> do putIState ist ; ierror err)

262 (\err -> do putIState ist ; ierror err)

262 Success tac -> do (_, e) <- elabStep e saveState

263 Success tac -> do (_, e) <- elabStep e saveState

263− (_, st) <- elabStep e (runTac True i fn tac)

264+ (_, st) <- elabStep e (runTac autoSolve i fn tac)

264-- trace (show (problems (proof st))) $

265-- trace (show (problems (proof st))) $

265 iPrintResult ""

266 iPrintResult ""

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

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

src/Idris/REPL.hs+2

@@ -932,6 +932,8 @@ process h fn (SetOpt ShowImpl) = setImpShow True

932process h fn (UnsetOpt ShowImpl) = setImpShow False

933process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

934process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

935+process h fn (SetOpt AutoSolve) = setAutoSolve True

936+process h fn (UnsetOpt AutoSolve) = setAutoSolve False

935

937

936process h fn (SetOpt _) = iPrintError "Not a valid option"

938process h fn (SetOpt _) = iPrintError "Not a valid option"

937process h fn (UnsetOpt _) = iPrintError "Not a valid option"

939process h fn (UnsetOpt _) = iPrintError "Not a valid option"

src/Idris/REPLParser.hs+1

@@ -107,6 +107,7 @@ pOption :: P.IdrisParser Opt

107pOption = do discard (P.symbol "errorcontext"); return ErrContext

108 <|> do discard (P.symbol "showimplicits"); return ShowImpl

109 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

110+ <|> do discard (P.symbol "autosolve"); return AutoSolve

110

111

111pConsoleWidth :: P.IdrisParser ConsoleWidth

112pConsoleWidth :: P.IdrisParser ConsoleWidth

112pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

113pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

test/Makefile+3−3

@@ -8,13 +8,13 @@ test: $(TESTS)

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

10test_java:

11− perl ./runtest.pl without buffer001 --codegen Java

11+ perl ./runtest.pl without sugar004 buffer001 --codegen Java

13test_js:

14− @perl ./runtest.pl without reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 --codegen node

14+ @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 --codegen node

16test_llvm:

17− @perl ./runtest.pl without io003 buffer001 --codegen llvm

17+ @perl ./runtest.pl without sugar004 io003 buffer001 --codegen llvm

19update:

20 /usr/bin/env perl ./runtest.pl all -u

test/sugar004/expectednew file+3

@@ -0,0 +1,3 @@

1+No arguments!

2+42

3+Too many arguments!

test/sugar004/runnew file+6

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

1+#!/usr/bin/env bash

2+idris $@ sugar004.idr -o sugar004

3+./sugar004

4+./sugar004 42

5+./sugar004 42 100

6+rm -f sugar004 *.ibc

test/sugar004/sugar004.idrnew file+36

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

1+module Main

3+import System

5+total

6+foo : Maybe Int -> Int

7+foo x = let Just x' = x | Nothing => 100 in x'

9+main : IO ()

10+main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

11+ | (x :: y :: _) => putStrLn "Too many arguments!"

12+ print (foo (Just (cast a)))

13+

14+{-

15+

16+let pat = val | <alternatives> in x'

17+

18+...becomes...

19+

20+case val of

21+ pat => x'

22+ <alternatives>

23+

24+do pat <- val | <alternatives>

25+ p

26+

27+...becomes...

28+

29+do x <- val

30+ case x of

31+ pat => p

32+ <alternatives>

33+

34+-}

35+

36+