db306ca · Idris-dev · git.iko.soy

CHANGELOG+12−9

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

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

55 type inference.

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

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

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

9−* Lots of performance patches for generated JavaScript

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

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

9+* Lots of performance patches for generated JavaScript.

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

11− or show the type of expressions

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

11+ or show the type of expressions.

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

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

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

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

15−||| Add two natural numbers

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

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

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

16+ ||| Add two natural numbers

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

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

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

1922

2023New in 0.9.11:

2124--------------

Makefile+1−1

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

3939 $(CABAL) install $(CABALFLAGS)

4040

4141linecount:

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

4343

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

4545doc: dist/setup-config

idris.cabal+8

@@ -221,6 +221,12 @@ Extra-source-files:

221221 test/reg036/run

222222 test/reg036/*.idr

223223 test/reg036/expected

224+ test/reg037/run

225+ test/reg037/*.idr

226+ test/reg037/expected

227+ test/reg038/run

228+ test/reg038/*.idr

229+ test/reg038/expected

224230

225231 test/basic001/run

226232 test/basic001/*.idr

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

434440 , Idris.DeepSeq

435441 , Idris.Delaborate

436442 , Idris.Docs

443+ , Idris.Docstrings

437444 , Idris.ElabDecls

438445 , Idris.ElabTerm

439446 , Idris.Error

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

500507 , ansi-wl-pprint

501508 , binary

502509 , bytestring

510+ , cheapskate

503511 , containers >= 0.5

504512 , directory

505513 , directory >= 1.2

libs/base/Decidable/Order.idr+3−4

@@ -26,10 +26,9 @@ class (Poset t to) => Ordered t (to : t -> t -> Type) where

2626class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where

2727 total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a

2828

29−class (Equivalence t eq) => Congruence t (eq : t -> t -> Type) where

29+class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where

3030 total congruent : (a : t) ->

3131 (b : t) ->

32− (f : t -> t) ->

3332 eq a b ->

3433 eq (f a) (f b)

3534

@@ -54,8 +53,8 @@ instance Preorder t ((=) {A = t} {B = t}) where

5453instance Equivalence t ((=) {A = t} {B = t}) where

5554 symmetric a b prf = sym prf

5655

57−instance Congruence t ((=) {A = t} {B = t}) where

58− congruent a b f = cong {a = a} {b = b} {f = f}

56+instance Congruence t f ((=) {A = t} {B = t}) where

57+ congruent a b = cong {a = a} {b = b} {f = f}

5958

6059--------------------------------------------------------------------------------

6160-- Natural numbers

libs/base/Language/Reflection.idr+2

@@ -180,6 +180,8 @@ data Tactic = Try Tactic Tactic

180180 -- ^ invoke the reflected rep. of another tactic

181181 | Reflect TT

182182 -- ^ turn a value into its reflected representation

183+ | ByReflection TT

184+ -- ^ use a %reflection function

183185 | Fill Raw

184186 -- ^ turn a raw value back into a term

185187 | Exact TT

libs/neweffects/Effect/Exception.idr+3

@@ -10,6 +10,9 @@ data Exception : Type -> Effect where

1010instance Handler (Exception a) Maybe where

1111 handle _ (Raise e) k = Nothing

1212

13+instance Handler (Exception a) List where

14+ handle _ (Raise e) k = []

15+

1316instance Show a => Handler (Exception a) IO where

1417 handle _ (Raise e) k = do print e

1518 believe_me (exit 1)

libs/neweffects/Effects.idr+7−2

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

171171

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

173173 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 =>

175175 res ->

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

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

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

226226eff env (lift prf effP) k

227227 = let env' = dropEnv env prf in

228228 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

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

231231eff env (catch prog handler) k

232232 = catch (eff env prog k)

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

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

266266effect' e {prf} = effect prf e

267267

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

268273

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

270275run {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

100100ffi :: String -> [String] -> String

101101ffi code args = let parsed = ffiParse code in

102102 case ffiError parsed of

103− Just err -> compileJS $ jsError err

103+ Just err -> error err

104104 Nothing -> renderFFI parsed args

105105 where

106106 ffiParse :: String -> [FFI]

107107 ffiParse "" = []

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

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

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

110110 ffiParse ('%':s:ss)

111111 | isDigit s =

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

113113 | otherwise =

114− [FFIError "Invalid positional argument"]

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

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

116116

117117

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

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

127127 renderFFI ((FFIArg i) : fs) args

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

130130

131131

132132compileJS :: JS -> String

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

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

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

19661966

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

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

1969+

19671970translateExpression (SForeign _ _ fun args) =

19681971 JSFFI fun (map generateWrapper args)

19691972 where

src/Idris/AbsSyntax.hs+18−5

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

99import Idris.Core.Typecheck

1010import Idris.AbsSyntaxTree

1111import Idris.Colours

12+import Idris.Docstrings

1213import Idris.IdeSlave

1314import IRTS.CodegenCommon

1415import Util.DynamicLinker

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

262263addCoercion n = do i <- getIState

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

264265

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

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

266267addDocStr n doc args

267268 = do i <- getIState

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

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

713714 let opt' = opts { opt_origerr = b }

714715 putIState $ i { idris_options = opt' }

715716

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+

716723setNoBanner :: Bool -> Idris ()

717724setNoBanner n = do i <- getIState

718725 let opts = idris_options i

@@ -1250,18 +1257,24 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12501257 | otherwise = x : dropAll xs ys

12511258 dropAll [] ys = []

12521259

1260+ -- Find names in argument position in a type, suitable for implicit

1261+ -- binding

1262+ -- Not the function position, but do everything else...

1263+ implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)

1264+ implNamesIn uv t = namesIn uv ist t

1265+

12531266 imps top env (PApp _ f as)

12541267 = do (decls, ns) <- get

12551268 let isn = concatMap (namesIn uvars ist) (map getTm as)

12561269 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12571270 imps top env (PPi (Imp l _ _) n ty sc)

1258− = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

1271+ = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

12591272 (decls , ns) <- get

12601273 put (PImp (getPriority ist ty) True l n Placeholder : decls,

12611274 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12621275 imps True (n:env) sc

12631276 imps top env (PPi (Exp l _ _) n ty sc)

1264− = do let isn = nub (namesIn uvars ist ty ++ case sc of

1277+ = do let isn = nub (implNamesIn uvars ty ++ case sc of

12651278 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12661279 _ -> [])

12671280 (decls, ns) <- get -- ignore decls in HO types

@@ -1269,7 +1282,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12691282 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12701283 imps True (n:env) sc

12711284 imps top env (PPi (Constraint l _) n ty sc)

1272− = do let isn = nub (namesIn uvars ist ty ++ case sc of

1285+ = do let isn = nub (implNamesIn uvars ty ++ case sc of

12731286 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12741287 _ -> [])

12751288 (decls, ns) <- get -- ignore decls in HO types

@@ -1277,7 +1290,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12771290 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12781291 imps True (n:env) sc

12791292 imps top env (PPi (TacImp l _ scr) n ty sc)

1280− = do let isn = nub (namesIn uvars ist ty ++ case sc of

1293+ = do let isn = nub (implNamesIn uvars ty ++ case sc of

12811294 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12821295 _ -> [])

12831296 (decls, ns) <- get -- ignore decls in HO types

src/Idris/AbsSyntaxTree.hs+34−30

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

77import Idris.Core.Evaluate

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

99import Idris.Core.Typecheck

10+import Idris.Docstrings

1011import IRTS.Lang

1112import IRTS.CodegenCommon

1213import Util.Pretty

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

5354 opt_cpu :: String,

5455 opt_optLevel :: Word,

5556 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

5759 }

5860 deriving (Show, Eq)

5961

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

7678 , opt_optLevel = 2

7779 , opt_cmdline = []

7880 , opt_origerr = False

81+ , opt_autoSolve = True

7982 }

8083

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

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

111114 idris_flags :: Ctxt [FnOpt],

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

113116 idris_calledgraph :: Ctxt [Name],

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

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

115118 idris_tyinfodata :: Ctxt TIData,

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

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

@@ -337,6 +340,7 @@ data Opt = Filename String

337340 | Client String

338341 | ShowOrigErr

339342 | AutoWidth -- ^ Automatically adjust terminal width

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

340344 deriving (Show, Eq)

341345

342346-- Parsed declarations

@@ -451,15 +455,15 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms

451455-- datatypes and typeclasses.

452456data PDecl' t

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

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

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

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

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

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

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

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

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

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

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

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

462− | PClass String SyntaxInfo FC

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

466+ | PClass Docstring SyntaxInfo FC

463467 [t] -- constraints

464468 Name

465469 [(Name, t)] -- parameters

@@ -513,7 +517,7 @@ deriving instance NFData PClause'

513517-- | Data declaration

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

515519 d_tcon :: t, -- ^ Type constructor

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

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

517521 }

518522 -- ^ Data declaration

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

@@ -738,7 +742,7 @@ type PTactic = PTactic' PTerm

738742

739743data PDo' t = DoExp FC t

740744 | DoBind FC Name t

741− | DoBindP FC t t

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

742746 | DoLet FC Name t t

743747 | DoLetP FC t t

744748 deriving (Eq, Functor)

@@ -750,7 +754,7 @@ deriving instance NFData PDo'

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

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

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

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

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

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

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

756760

@@ -949,9 +953,9 @@ inferTy = sMN 0 "__Infer"

949953inferCon = sMN 0 "__infer"

950954inferDecl = PDatadecl inferTy

951955 PType

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

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

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

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

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

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

955959inferOpts = []

956960

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

@@ -979,7 +983,7 @@ primNames = [unitTy, unitCon,

979983unitTy = sMN 0 "__Unit"

980984unitCon = sMN 0 "__II"

981985unitDecl = PDatadecl unitTy PType

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

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

983987unitOpts = [DefaultEliminator]

984988

985989falseTy = sMN 0 "__False"

@@ -989,12 +993,12 @@ falseOpts = []

989993pairTy = sMN 0 "__Pair"

990994pairCon = sMN 0 "__MkPair"

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

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

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

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

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

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

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

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

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

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

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

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

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

9981002 where n a = sMN 0 a

9991003pairOpts = []

10001004

@@ -1003,21 +1007,21 @@ eqCon = sUN "refl"

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

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

10051009 PType)

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

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

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

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

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

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

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

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

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

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

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

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

10121016 where n a = sMN 0 a

10131017eqOpts = []

10141018

10151019elimName = sUN "__Elim"

10161020elimMethElimTy = sUN "__elimTy"

10171021elimMethElim = sUN "elim"

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

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

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

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

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

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

10211025

10221026-- Defined in builtins.idr

10231027sigmaTy = sUN "Exists"

@@ -1324,7 +1328,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

13241328 where strName (UN n) = T.unpack n

13251329 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

13261330 | otherwise = strName n

1327− strName (MN i s) = T.unpack s

1331+ strName (MN i s) = T.unpack s

13281332 strName other = show other

13291333

13301334

src/Idris/Completion.hs+5−1

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

108108

109109completeOption :: CompletionFunc Idris

110110completeOption = 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+ ]

112116

113117completeConsoleWidth :: CompletionFunc Idris

114118completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/DSL.hs+2−2

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

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

5858 block b (DoBind fc n tm : rest)

5959 = 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)

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

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

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

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

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

6565 = PLet n ty tm (block b rest)

6666 block b (DoLetP fc p tm : rest)

src/Idris/DeepSeq.hs+43−1

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

66

77import Control.DeepSeq

88

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+

951-- All generated by 'derive'

1052

1153instance NFData Forceability where

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

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

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

228270 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` ()

230272 rnf (DoLet x1 x2 x3 x4)

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

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

src/Idris/Delaborate.hs+10−7

@@ -100,11 +100,14 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

100100 | n == eqTy = PEq un (de env [] l) (de env [] r)

101101 | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder

102102 (de env [] r)

103− deFn env (P _ n _) args | not mvs

104− = case lookup n (idris_metavars ist) of

105− Just (Just _, mi, _) ->

106− mkMVApp n (drop mi (map (de env []) args))

107− _ -> mkPApp n (map (de env []) args)

103+ deFn env f@(P _ n _) args

104+ | n `elem` map snd env

105+ = PApp un (de env [] f) (map pexp (map (de env []) args))

106+ deFn env (P _ n _) args

107+ | not mvs = case lookup n (idris_metavars ist) of

108+ Just (Just _, mi, _) ->

109+ mkMVApp n (drop mi (map (de env []) args))

110+ _ -> mkPApp n (map (de env []) args)

108111 | otherwise = mkPApp n (map (de env []) args)

109112 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

110113

@@ -113,7 +116,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

113116 mkMVApp n args

114117 = PApp un (PMetavar n) (map pexp args)

115118 mkPApp n args

116− | [imps] <- lookupCtxt n (idris_implicits ist)

119+ | Just imps <- lookupCtxtExact n (idris_implicits ist)

117120 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

118121 | otherwise = PApp un (PRef un n) (map pexp args)

119122

@@ -233,7 +236,7 @@ pprintErr' i (ReflectionFailed msg err) =

233236 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

234237

235238annName :: Name -> Doc OutputAnnotation

236−annName n = annName' n (show n)

239+annName n = annName' n (showbasic n)

237240

238241annName' :: Name -> String -> Doc OutputAnnotation

239242annName' n str = annotate (AnnName n Nothing Nothing) (text str)

src/Idris/Docs.hs+15−13

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

1+{-# LANGUAGE PatternGuards #-}

12module Idris.Docs where

23

34import Idris.AbsSyntax

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

56import Idris.Delaborate

67import Idris.Core.TT

78import Idris.Core.Evaluate

9+import Idris.Docstrings

810

911import Util.Pretty

1012

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

1315

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

1517

16−data FunDoc = FD Name String

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

18+data FunDoc = FD Name Docstring

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

1820 PTerm -- function type

1921 (Maybe Fixity)

2022 deriving Show

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

2224data Docs = FunDoc FunDoc

2325 | DataDoc FunDoc -- type constructor docs

2426 [FunDoc] -- data constructor docs

25− | ClassDoc Name String -- class docs

27+ | ClassDoc Name Docstring -- class docs

2628 [FunDoc] -- method docs

2729 deriving Show

2830

29−showDoc "" = empty

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

31+showDoc d | nullDocstring d = empty

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

3133

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

3335pprintFD 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 <$>

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

3638 let argshow = showArgs args [] in

3739 if not (null argshow)

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

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

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

4345 pprintPTerm imp bnd ty <>

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

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

4547 :

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

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

4850 = text "Class constraint" <+>

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

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

5052 :

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

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

53− | not (null doc)

55+ | Just d' <- d

5456 = text "(implicit)" <+>

5557 bindingOf n True <+> colon <+>

5658 pprintPTerm imp bnd ty <>

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

59+ showDoc d' <> line

5860 :

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

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

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

9395 = do i <- getIState

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

9597 [str] -> fst str

96− _ -> ""

98+ _ -> emptyDocstring

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

98100 return (ClassDoc n docstr mdocs)

99101

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

102104 = do i <- getIState

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

104106 [d] -> d

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

107+ _ -> noDocs

106108 let ty = delabTy i n

107109 let args = getPArgNames ty argDocs

108110 let infixes = idris_infixes i

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

116118 funName (UN n) = str n

117119 funName (NS n _) = funName n

118120

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

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

120122getPArgNames (PPi plicity name ty body) ds =

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

122124getPArgNames _ _ = []

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

5+

6+import qualified Cheapskate as C

7+import qualified Cheapskate.Types as CT

8+

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+61−39

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

2626import Idris.Core.Typecheck

2727import Idris.Core.CaseTree

2828

29+import Idris.Docstrings

30+

2931import Control.DeepSeq

3032import Control.Monad

3133import Control.Monad.State.Strict as State

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

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

6466

6567-- | 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)] ->

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

6870elabType = elabType' False

6971

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

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

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

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

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

7476 n = liftname info n_in in -}

@@ -76,12 +78,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

7678 ctxt <- getContext

7779 i <- getIState

7880

79− logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'

81+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

8082 ty' <- addUsingConstraints syn fc ty'

8183 ty' <- implicit syn n ty'

8284

8385 let ty = addImpl i ty'

84− logLvl 1 $ show n ++ " type " ++ showTmImpls ty

86+ logLvl 3 $ show n ++ " type " ++ showTmImpls ty

8587 ((tyT, defer, is), log) <-

8688 tclift $ elaborate ctxt n (TType (UVal 0)) []

8789 (errAt "type of " n (erun fc (build i info False [] n ty)))

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

171173 tyIsHandler _ = False

172174

173175

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

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

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

176178elabPostulate info syn doc fc opts n ty

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

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

195197 -- remove it from the deferred definitions list

196198 solveDeferred n

197199

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

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

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

200202 = do let codata = Codata `elem` opts

201203 iLOG (show (fc, doc))

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

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

258260 updateContext (setMetaInformation n metainf)

259261 mapM_ (checkPositive n) cons

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

261− else return ()

262+ if DefaultEliminator `elem` opts

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

264+ else return ()

262265 where

263266 checkDefinedAs fc n t ctxt

264267 = case lookupDef n ctxt of

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

322325

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

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

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

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

326329 ElabInfo -> EliminatorState ()

327330elabEliminator paramPos n ty cons info = do

328331 elimLog $ "Elaborating eliminator"

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

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

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

341344 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

343346 let clauseConsElimArgs = map getPiName consTerms

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

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

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

488491 splitArgPms _ = ([],[])

489492

490493

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

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

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

493496 i <- State.lift getIState

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

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

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

504507 _ -> return implargs

505508

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

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

508511 let cons' = replaceParams paramPos generalParameters ty

509512 let (args, resTy) = splitPi cons'

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

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

540543 convertImplPi _ = Nothing

541544

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

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

544547 let cons' = replaceParams paramPos generalParameters ty

545548 let (args, resTy) = splitPi cons'

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

561564

562565elabPrims :: Idris ()

563566elabPrims = 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)

565568 (zip

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

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

@@ -656,7 +659,7 @@ elabProvider info syn fc what n ty tm

656659 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)

657660 [Erased, e])

658661 let rhs' = normalise ctxt [] rhs

659− logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

662+ logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

660663

661664 -- Extract the provided term or postulate from the type provider

662665 provided <- getProvided fc rhs'

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

665668 Provide tm

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

667670 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

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

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

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

671674 | otherwise ->

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

673676 Postulate

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

675678 do -- Add the postulate

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

677− logLvl 1 $ "Elaborated provided postulate " ++ show n

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

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

678681 | otherwise ->

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

680683

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

724727 addIBC (IBCTrans (clhs_tm, crhs_tm))

725728

726729

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

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

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

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

729732elabRecord info syn doc fc tyn ty cdoc cn cty

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

731734 cty' <- implicit syn cn cty

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

797800

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

799802 = do let pn = expandNS syn pn_in

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

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

801804 (PPi expl rec recty

802805 (substMatches substs pty))

803806 let pls = repeat Placeholder

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

818821 let valname = sMN 0 "updateval"

819822 let pt = k (PPi expl pn pty

820823 (PPi expl rec recty recty))

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

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

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

823826 let lhsArgs = pls

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

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

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

835838

836839elabCon :: 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)

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

839842 = do checkUndefined fc n

840843 ctxt <- getContext

@@ -988,7 +991,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

988991 simpleCase tcase False reflect CompileTime fc atys pdef

989992 cov <- coverage

990993 pmissing <-

991− if cov

994+ if cov && not (hasDefault cs)

992995 then do missing <- genClauses fc n (map getLHS pdef) cs

993996 -- missing <- genMissing n scargs sc

994997 missing' <- filterM (checkPossible info fc True n) missing

@@ -1092,6 +1095,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

10921095 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)

10931096 depat acc x = (acc, x)

10941097

1098+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs

1099+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args

1100+ hasDefault _ = False

1101+

10951102 getLHS (_, l, _) = l

10961103

10971104 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,

@@ -1162,10 +1169,10 @@ elabPE info fc caller r =

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

11631170 (showTmImpls lhs ++ " = " ++

11641171 showTmImpls rhs)) pats)

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

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

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

11671174 elabClauses info fc opts newnm def

1168− logLvl 1 $ "Specialised " ++ show newnm)

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

11691176 -- if it doesn't work, just don't specialise. Could happen for lots

11701177 -- of valid reasons (e.g. local variables in scope which can't be

11711178 -- lifted out).

@@ -1419,7 +1426,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

14191426 -- Elaborate those with a type *before* RHS, those without *after*

14201427 let (wbefore, wafter) = sepBlocks wb

14211428

1422− logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1429+ logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

14231430 mapM_ (elabDecl' EAll info) wbefore

14241431 -- Now build the RHS, using the type of the LHS as the goal.

14251432 i <- getIState -- new implicits from where block

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

15631570 _ -> []

15641571 let params = getParamsInType i [] fn_is fn_ty

15651572 let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1566− logLvl 1 ("LHS: " ++ show lhs)

1573+ logLvl 2 ("LHS: " ++ show lhs)

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

15681575 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

15691576 (errAt "left hand side of with in " fname

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

17211728

17221729data MArgTy = IA | EA | CA deriving Show

17231730

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

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

17251732 FC -> [PTerm] ->

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

17271734elabClass info syn doc fc constraints tn ps ds

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

17481755 let cty = impbind ps $ conbind constraints

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

17501757 constraint

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

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

17521759 let ddecl = PDatadecl tn tty cons

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

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

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

18031810 case lookup n mtys of

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

18051812 let ds = map (decorateid defaultdec)

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

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

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

18081815 iLOG (show ds)

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

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

18411848 addInstance False conn' cfn

18421849 addIBC (IBCInstance False conn' cfn)

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

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

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

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

18461853

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

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

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

19061913 let iname = mkiname n ps expn

19071914 when (what /= EDefns) $ do

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

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

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

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

19111918 case expn of

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

19211928 -- get the implicit parameters that need passing through to the

19221929 -- where block

19231930 wparams <- mapM (\p -> case p of

1924− PApp _ _ args -> getWParams args

1931+ PApp _ _ args -> getWParams (map getTm args)

19251932 _ -> return []) ps

19261933 let pnames = map pname (concat (nub wparams))

19271934 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

@@ -1947,9 +1954,24 @@ elabInstance info syn what fc cs n ps t expn ds = do

19471954 logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

19481955 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

19491956 show (concat (nub wparams))

1950− let lhs = PRef fc iname

1957+

1958+ -- Bring variables in instance head into scope

1959+ ist <- getIState

1960+ let headVars = mapMaybe (\p -> case p of

1961+ PRef _ n ->

1962+ case lookupTy n (tt_ctxt ist) of

1963+ [] -> Just n

1964+ _ -> Nothing

1965+ _ -> Nothing) ps

1966+-- let lhs = PRef fc iname

1967+ let lhs = PApp fc (PRef fc iname)

1968+ (map (\n -> pimp n (PRef fc n) True) headVars)

19511969 let rhs = PApp fc (PRef fc (instanceName ci))

19521970 (map (pexp . mkMethApp) mtys)

1971+

1972+ logLvl 5 $ "Instance LHS " ++ show lhs

1973+ logLvl 5 $ "Instance RHS " ++ show rhs

1974+

19531975 let idecls = [PClauses fc [Dictionary] iname

19541976 [PClause fc iname lhs [] rhs wb]]

19551977 iLOG (show idecls)

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

20312053

20322054 getWParams [] = return []

20332055 getWParams (p : ps)

2034− | PRef _ n <- getTm p

2056+ | PRef _ n <- p

20352057 = do ps' <- getWParams ps

20362058 ctxt <- getContext

20372059 case lookupP n ctxt of

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

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

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

20442066

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

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

20462068

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

20482070 conbind [] x = x

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

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

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

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

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

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

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

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

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

src/Idris/ElabTerm.hs+2

@@ -1205,6 +1205,8 @@ reifyApp ist t [t']

12051205 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

12061206reifyApp ist t [t']

12071207 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')

1208+reifyApp ist t [t']

1209+ | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')

12081210reifyApp _ t [t']

12091211 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

12101212reifyApp ist t [t']

src/Idris/IBC.hs+93−8

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

99import Idris.Imports

1010import Idris.Error

1111import Idris.Delaborate

12+import Idris.Docstrings

13+

14+import qualified Cheapskate.Types as CT

1215

1316import Data.Binary

1417import Data.Vector.Binary

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

2528import Util.Zlib (decompressEither)

2629

2730ibcVersion :: Word8

28−ibcVersion = 62

31+ibcVersion = 63

2932

3033

3134data IBCFile = IBCFile { ver :: Word8,

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

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

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

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

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

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

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

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

5861 ibc_coercions :: [Name],

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

405408 update (Proj t i) = Proj (update t) i

406409 update t = t

407410

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

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

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

410413

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

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

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

462465 ++ idris_metavars i }

463466

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+

464547----- Generated by 'derive'

465548

466549instance Binary SizeChange where

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

18781961 put x1

18791962 put x2

18801963 put x3

1881− DoBindP x1 x2 x3 -> do putWord8 2

1882− put x1

1883− put x2

1884− put x3

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

1965+ put x1

1966+ put x2

1967+ put x3

1968+ put x4

18851969 DoLet x1 x2 x3 x4 -> do putWord8 3

18861970 put x1

18871971 put x2

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

19041988 2 -> do x1 <- get

19051989 x2 <- get

19061990 x3 <- get

1907− return (DoBindP x1 x2 x3)

1991+ x4 <- get

1992+ return (DoBindP x1 x2 x3 x4)

19081993 3 -> do x1 <- get

19091994 x2 <- get

19101995 x3 <- get

src/Idris/ParseData.hs+8−6

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

2020import Idris.Core.TT

2121import Idris.Core.Evaluate

2222

23+import Idris.Docstrings

24+

2325import Control.Applicative

2426import Control.Monad

2527import Control.Monad.State.Strict

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

4143-}

4244record :: SyntaxInfo -> IdrisParser PDecl

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

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

46+ doc <- option noDocs docComment

4547 acc <- optional accessibility

4648 reserved "record"

4749 return (doc, acc))

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

103105-}

104106data_ :: SyntaxInfo -> IdrisParser PDecl

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

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

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

107109 pushIndent

108110 acc <- optional accessibility

109111 elim <- dataOpts []

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

160162{- | Parses a type constructor declaration

161163 Constructor ::= DocComment? FnName TypeSig;

162164-}

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

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

164166constructor syn

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

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

166168 cn_in <- fnName; fc <- getFC

167169 let cn = expandNS syn cn_in

168170 lchar ':'

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

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

178180 SimpleConstructor ::= FnName SimpleExpr* DocComment?

179181-}

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

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

181183simpleConstructor syn

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

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

183185 cn_in <- fnName

184186 let cn = expandNS syn cn_in

185187 fc <- getFC

src/Idris/ParseExpr.hs+25−6

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

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

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

169169 : upd (dropn n ns) ds

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

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

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

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

171173 : upd ns ds

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

173175 : upd ns ds

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

736738@

737739 -}

738740let_ :: SyntaxInfo -> IdrisParser PTerm

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

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

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

741743 lchar '='

742744 v <- expr syn

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

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

743747 reserved "in"; sc <- expr syn

744− return (PLet n ty v sc))

748+ case ts of

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

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

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

746752 symbol "="; v <- expr syn

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

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

747755 reserved "in"; sc <- expr syn

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

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

749757 <?> "let binding"

750758

751759{- | Parses a quote goal

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

967975 symbol "<-"

968976 fc <- getFC

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

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

972983 symbol "<-"

973984 fc <- getFC

974985 e <- expr syn;

975− return (DoBindP fc i e))

986+ option (DoBindP fc i e [])

987+ (do lchar '|'

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

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

976990 <|> do e <- expr syn

977991 fc <- getFC

978992 return (DoExp fc e)

979993 <?> "do block expression"

980994

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

996+ symbol "=>"

997+ r <- expr' syn

998+ return (l, r)

999+

9811000{- | Parses an expression in idiom brackets

9821001@

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

src/Idris/ParseHelpers.hs+14−10

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

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

1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, OverlappingInstances, StandaloneDeriving #-}

22module Idris.ParseHelpers where

33

44import Prelude hiding (pi)

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

1616import Idris.Core.TT

1717import Idris.Core.Evaluate

1818import Idris.Delaborate (pprintErr)

19+import Idris.Docstrings

1920

2021import qualified Util.Pretty as Pretty (text)

2122

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

4142type IdrisParser = StateT IState IdrisInnerParser

4243

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

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

45+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

46+

47+deriving instance Parsing IdrisInnerParser

4548

4649instance TokenParsing IdrisParser where

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

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

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

146149

147150@

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

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

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

150152 ;

151153@

152154 -}

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

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

154156docComment = do dc <- pushIndent *> docCommentLine

155157 rest <- many (indented docCommentLine)

156158 args <- many (indented argDocCommentLine)

157159 popIndent

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

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

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

159162

160163 where docCommentLine :: MonadicParsing m => m String

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

162− many (satisfy isSpace)

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

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

165+ many (satisfy (==' '))

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

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

168+ return $ first:res)

165169 eol ; someSpace

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

170+ return contents)-- ++ concat rest))

167171 <?> ""

168172 argDocCommentLine = do string "|||"

169173 many (satisfy isSpace)

src/Idris/ParseOps.hs−1

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

5959 indentPropHolds gtProp

6060 reservedOp name

6161 indentPropHolds gtProp

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

6362 return (f fc))

6463

6564-- | Prefix operator

src/Idris/Parser.hs+7−5

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

3535import Idris.ParseExpr

3636import Idris.ParseData

3737

38+import Idris.Docstrings

39+

3840import Paths_idris

3941

4042import Util.DynamicLinker

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

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

316318 pushIndent

317319 ist <- get

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

320+ doc <- option noDocs docComment

319321 ist <- get

320322 let initOpts = if default_total ist

321323 then [TotalFn]

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

413415@

414416-}

415417postulate :: SyntaxInfo -> IdrisParser PDecl

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

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

417419 pushIndent

418420 reserved "postulate"

419421 return doc

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

561563-}

562564class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

566+ doc <- option noDocs docComment

565567 acc <- optional accessibility

566568 return (doc, acc))

567569 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

10031005 mapM_ (addNameHint ty') ns

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

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

1006− fn <- iName []

1007− arg <- iName []

1008+ fn <- fnName

1009+ arg <- fnName

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

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

10101012 ns' <- mapM disambiguate ns

src/Idris/Prover.hs+2−1

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

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

165165ploop fn d prompt prf e h

166166 = do i <- getIState

167+ let autoSolve = opt_autoSolve (idris_options i)

167168 when d $ dumpState i (proof e)

168169 (x, h') <-

169170 case idris_outputmode i of

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

260261 return (False, e, False, prf))

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

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

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

265266 iPrintResult ""

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

src/Idris/REPL.hs+2

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

932932process h fn (UnsetOpt ShowImpl) = setImpShow False

933933process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

934934process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

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

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

935937

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

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

src/Idris/REPLParser.hs+1

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

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

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

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

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

110111

111112pConsoleWidth :: P.IdrisParser ConsoleWidth

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

test/Makefile+3−3

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

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

99

1010test_java:

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

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

1212

1313test_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

1515

1616test_llvm:

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

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

1818

1919update:

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

test/reg038/expectednew file

No changes to the content.

test/reg038/reg038.idrnew file+17

@@ -0,0 +1,17 @@

1+class C t (f : t -> t) (r : t -> t -> Type) where

2+ g : (a : t) -> r (f a) (f a) -> r (f a) (f a)

3+

4+data Foo : {t : Type} -> t -> t -> Type where

5+ MkFoo : {t : Type} -> {x : t} -> {y : t} -> Foo x y

6+

7+instance C t f (Foo {t = t}) where

8+ g x = id

9+

10+data Bar : {t1 : Type} -> {t2 : Type} -> t1 -> t2 -> Type where

11+ MkBar : {x : t1} -> Bar x x

12+

13+instance C s f (Bar {t1 = s} {t2 = s}) where

14+ g x = id

15+

16+instance C s f ((=) {A = s} {B = s}) where

17+ g x = id

test/reg038/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --check reg038.idr

3+rm -f *.ibc

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

2+

3+import System

4+

5+total

6+foo : Maybe Int -> Int

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

8+

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+