db306ca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/parserspanning

db306caAhmad Salim Al-Sibahi13 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+8

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

221 test/reg036/run

222 test/reg036/*.idr

223 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

224

230

225 test/basic001/run

231 test/basic001/run

226 test/basic001/*.idr

232 test/basic001/*.idr

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

434 , Idris.DeepSeq

440 , Idris.DeepSeq

435 , Idris.Delaborate

441 , Idris.Delaborate

436 , Idris.Docs

442 , Idris.Docs

443+ , Idris.Docstrings

437 , Idris.ElabDecls

444 , Idris.ElabDecls

438 , Idris.ElabTerm

445 , Idris.ElabTerm

439 , Idris.Error

446 , Idris.Error

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

500 , ansi-wl-pprint

507 , ansi-wl-pprint

501 , binary

508 , binary

502 , bytestring

509 , bytestring

510+ , cheapskate

503 , containers >= 0.5

511 , containers >= 0.5

504 , directory

512 , directory

505 , directory >= 1.2

513 , 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

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

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

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

30 total congruent : (a : t) ->

31 (b : t) ->

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

33 eq a b ->

32 eq a b ->

34 eq (f a) (f b)

33 eq (f a) (f b)

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

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

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

55 symmetric a b prf = sym prf

54 symmetric a b prf = sym prf

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

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

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

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

60--------------------------------------------------------------------------------

59--------------------------------------------------------------------------------

61-- Natural numbers

60-- Natural numbers

libs/base/Language/Reflection.idr+2

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

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

181 | Reflect TT

182 -- ^ turn a value into its reflected representation

183+ | ByReflection TT

184+ -- ^ use a %reflection function

183 | Fill Raw

185 | Fill Raw

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

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

185 | Exact TT

187 | Exact TT

libs/neweffects/Effect/Exception.idr+3

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

10instance Handler (Exception a) Maybe where

11 handle _ (Raise e) k = Nothing

13+instance Handler (Exception a) List where

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

15+

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

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

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

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

15 believe_me (exit 1)

18 believe_me (exit 1)

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+18−5

@@ -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

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

1250 | otherwise = x : dropAll xs ys

1257 | otherwise = x : dropAll xs ys

1251 dropAll [] ys = []

1258 dropAll [] ys = []

1252

1259

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+

1253 imps top env (PApp _ f as)

1266 imps top env (PApp _ f as)

1254 = do (decls, ns) <- get

1267 = do (decls, ns) <- get

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

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

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

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

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

1270 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]

1259 (decls , ns) <- get

1272 (decls , ns) <- get

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

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

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

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

1262 imps True (n:env) sc

1275 imps True (n:env) sc

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

1276 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

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

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

1266 _ -> [])

1279 _ -> [])

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

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

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

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

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

1270 imps True (n:env) sc

1283 imps True (n:env) sc

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

1284 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

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

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

1274 _ -> [])

1287 _ -> [])

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

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

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

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

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

1278 imps True (n:env) sc

1291 imps True (n:env) sc

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

1292 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

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

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

1282 _ -> [])

1295 _ -> [])

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

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

src/Idris/AbsSyntaxTree.hs+34−30

@@ -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

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

337 | Client String

340 | Client String

338 | ShowOrigErr

341 | ShowOrigErr

339 | AutoWidth -- ^ Automatically adjust terminal width

342 | AutoWidth -- ^ Automatically adjust terminal width

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

340 deriving (Show, Eq)

344 deriving (Show, Eq)

341

345

342-- Parsed declarations

346-- Parsed declarations

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

451-- datatypes and typeclasses.

455-- datatypes and typeclasses.

452data PDecl' t

456data PDecl' t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

462− | PClass String SyntaxInfo FC

466+ | PClass Docstring SyntaxInfo FC

463 [t] -- constraints

467 [t] -- constraints

464 Name

468 Name

465 [(Name, t)] -- parameters

469 [(Name, t)] -- parameters

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

513-- | Data declaration

517-- | Data declaration

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

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

515 d_tcon :: t, -- ^ Type constructor

519 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

517 }

521 }

518 -- ^ Data declaration

522 -- ^ Data declaration

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

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

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

738

742

739data PDo' t = DoExp FC t

743data PDo' t = DoExp FC t

740 | DoBind FC Name t

744 | DoBind FC Name t

741− | DoBindP FC t t

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

742 | DoLet FC Name t t

746 | DoLet FC Name t t

743 | DoLetP FC t t

747 | DoLetP FC t t

744 deriving (Eq, Functor)

748 deriving (Eq, Functor)

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

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

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

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

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

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

756 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

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

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

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

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

756

760

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

949inferCon = sMN 0 "__infer"

953inferCon = sMN 0 "__infer"

950inferDecl = PDatadecl inferTy

954inferDecl = PDatadecl inferTy

951 PType

955 PType

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

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

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

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

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

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

955inferOpts = []

959inferOpts = []

956

960

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

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

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

979unitTy = sMN 0 "__Unit"

983unitTy = sMN 0 "__Unit"

980unitCon = sMN 0 "__II"

984unitCon = sMN 0 "__II"

981unitDecl = PDatadecl unitTy PType

985unitDecl = PDatadecl unitTy PType

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

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

983unitOpts = [DefaultEliminator]

987unitOpts = [DefaultEliminator]

984

988

985falseTy = sMN 0 "__False"

989falseTy = sMN 0 "__False"

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

989pairTy = sMN 0 "__Pair"

993pairTy = sMN 0 "__Pair"

990pairCon = sMN 0 "__MkPair"

994pairCon = sMN 0 "__MkPair"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

998 where n a = sMN 0 a

1002 where n a = sMN 0 a

999pairOpts = []

1003pairOpts = []

1000

1004

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

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

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

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

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

1005 PType)

1009 PType)

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

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

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

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

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

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

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

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

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

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

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

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

1012 where n a = sMN 0 a

1016 where n a = sMN 0 a

1013eqOpts = []

1017eqOpts = []

1014

1018

1015elimName = sUN "__Elim"

1019elimName = sUN "__Elim"

1016elimMethElimTy = sUN "__elimTy"

1020elimMethElimTy = sUN "__elimTy"

1017elimMethElim = sUN "elim"

1021elimMethElim = sUN "elim"

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

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

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

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

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

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

1021

1025

1022-- Defined in builtins.idr

1026-- Defined in builtins.idr

1023sigmaTy = sUN "Exists"

1027sigmaTy = sUN "Exists"

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

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

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

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

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

1326 | otherwise = strName n

1330 | otherwise = strName n

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

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

1328 strName other = show other

1332 strName other = show other

1329

1333

1330

1334

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/Delaborate.hs+10−7

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

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

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

102 (de env [] r)

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

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

104− = case lookup n (idris_metavars ist) of

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

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

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

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

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

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

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

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

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

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

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

110

113

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

113 mkMVApp n args

116 mkMVApp n args

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

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

115 mkPApp n args

118 mkPApp n args

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

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

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

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

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

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

119

122

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

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

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

234

237

235annName :: Name -> Doc OutputAnnotation

238annName :: Name -> Doc OutputAnnotation

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

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

237

240

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

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

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

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

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

@@ -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 -}

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

76 ctxt <- getContext

78 ctxt <- getContext

77 i <- getIState

79 i <- getIState

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

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

80 ty' <- addUsingConstraints syn fc ty'

82 ty' <- addUsingConstraints syn fc ty'

81 ty' <- implicit syn n ty'

83 ty' <- implicit syn n ty'

83 let ty = addImpl i ty'

85 let ty = addImpl i ty'

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

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

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

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

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

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

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

89 (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

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

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

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

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

657 [Erased, e])

660 [Erased, e])

658 let rhs' = normalise ctxt [] rhs

661 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

660

663

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

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

662 provided <- getProvided fc rhs'

665 provided <- getProvided fc rhs'

@@ -665,16 +668,16 @@ 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 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

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

671 | otherwise ->

674 | otherwise ->

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

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

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

680

683

@@ -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

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

988 simpleCase tcase False reflect CompileTime fc atys pdef

991 simpleCase tcase False reflect CompileTime fc atys pdef

989 cov <- coverage

992 cov <- coverage

990 pmissing <-

993 pmissing <-

991− if cov

994+ if cov && not (hasDefault cs)

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

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

993 -- missing <- genMissing n scargs sc

996 -- missing <- genMissing n scargs sc

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

997 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

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

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

1093 depat acc x = (acc, x)

1096 depat acc x = (acc, x)

1094

1097

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

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

1100+ hasDefault _ = False

1101+

1095 getLHS (_, l, _) = l

1102 getLHS (_, l, _) = l

1096

1103

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

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

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

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

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

1163 (showTmImpls lhs ++ " = " ++

1170 (showTmImpls lhs ++ " = " ++

1164 showTmImpls rhs)) pats)

1171 showTmImpls rhs)) pats)

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

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

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

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

1167 elabClauses info fc opts newnm def

1174 elabClauses info fc opts newnm def

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

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

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

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

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

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

1171 -- lifted out).

1178 -- lifted out).

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

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

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

1420 let (wbefore, wafter) = sepBlocks wb

1427 let (wbefore, wafter) = sepBlocks wb

1421

1428

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

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

1423 mapM_ (elabDecl' EAll info) wbefore

1430 mapM_ (elabDecl' EAll info) wbefore

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

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

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

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

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

1563 _ -> []

1570 _ -> []

1564 let params = getParamsInType i [] fn_is fn_ty

1571 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

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

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

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

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

1721

1728

1722data MArgTy = IA | EA | CA deriving Show

1729data MArgTy = IA | EA | CA deriving Show

1723

1730

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

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

1725 FC -> [PTerm] ->

1732 FC -> [PTerm] ->

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

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

1727elabClass info syn doc fc constraints tn ps ds

1734elabClass info syn doc fc constraints tn ps ds

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

1748 let cty = impbind ps $ conbind constraints

1755 let cty = impbind ps $ conbind constraints

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

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

1750 constraint

1757 constraint

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

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

1752 let ddecl = PDatadecl tn tty cons

1759 let ddecl = PDatadecl tn tty cons

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

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

1754 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

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

1803 case lookup n mtys of

1810 case lookup n mtys of

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

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

1805 let ds = map (decorateid defaultdec)

1812 let ds = map (decorateid defaultdec)

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

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

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

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

1808 iLOG (show ds)

1815 iLOG (show ds)

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

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

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

1841 addInstance False conn' cfn

1848 addInstance False conn' cfn

1842 addIBC (IBCInstance False conn' cfn)

1849 addIBC (IBCInstance False conn' cfn)

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

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

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

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

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

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

1846

1853

1847 -- 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

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

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

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

1906 let iname = mkiname n ps expn

1913 let iname = mkiname n ps expn

1907 when (what /= EDefns) $ do

1914 when (what /= EDefns) $ do

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

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

1909 -- 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,

1910 -- 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

1911 case expn of

1918 case expn of

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

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

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

1922 -- where block

1929 -- where block

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

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

1924− PApp _ _ args -> getWParams args

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

1925 _ -> return []) ps

1932 _ -> return []) ps

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

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

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

1934 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

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

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

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

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

1949 show (concat (nub wparams))

1956 show (concat (nub wparams))

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

1950− let lhs = PRef fc iname

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

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

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

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

1952 (map (pexp . mkMethApp) mtys)

1970 (map (pexp . mkMethApp) mtys)

1971+

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

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

1974+

1953 let idecls = [PClauses fc [Dictionary] iname

1975 let idecls = [PClauses fc [Dictionary] iname

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

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

1955 iLOG (show idecls)

1977 iLOG (show idecls)

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

2031

2053

2032 getWParams [] = return []

2054 getWParams [] = return []

2033 getWParams (p : ps)

2055 getWParams (p : ps)

2034− | PRef _ n <- getTm p

2056+ | PRef _ n <- p

2035 = do ps' <- getWParams ps

2057 = do ps' <- getWParams ps

2036 ctxt <- getContext

2058 ctxt <- getContext

2037 case lookupP n ctxt of

2059 case lookupP n ctxt of

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

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

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

2043 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

2044

2066

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

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

2046

2068

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

2048 conbind [] x = x

2070 conbind [] x = x

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

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

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

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

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

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

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

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

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

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

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

2294 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

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

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

src/Idris/ElabTerm.hs+2

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

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

1206reifyApp ist t [t']

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

1208+reifyApp ist t [t']

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

1208reifyApp _ t [t']

1210reifyApp _ t [t']

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

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

1210reifyApp ist t [t']

1212reifyApp ist t [t']

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−10

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

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

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

2module Idris.ParseHelpers where

4import Prelude hiding (pi)

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

16import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19+import Idris.Docstrings

20import qualified Util.Pretty as Pretty (text)

21import qualified Util.Pretty as Pretty (text)

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

41type IdrisParser = StateT IState IdrisInnerParser

42type IdrisParser = StateT IState IdrisInnerParser

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

44newtype 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

46instance TokenParsing IdrisParser where

49instance TokenParsing IdrisParser where

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

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

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

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

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

146

149

147@

150@

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

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

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

150 ;

152 ;

151@

153@

152 -}

154 -}

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

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

154docComment = do dc <- pushIndent *> docCommentLine

156docComment = do dc <- pushIndent *> docCommentLine

155 rest <- many (indented docCommentLine)

157 rest <- many (indented docCommentLine)

156 args <- many (indented argDocCommentLine)

158 args <- many (indented argDocCommentLine)

157 popIndent

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

159

162

160 where docCommentLine :: MonadicParsing m => m String

163 where docCommentLine :: MonadicParsing m => m String

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

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

162− many (satisfy isSpace)

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

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

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

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

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

168+ return $ first:res)

165 eol ; someSpace

169 eol ; someSpace

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

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

167 <?> ""

171 <?> ""

168 argDocCommentLine = do string "|||"

172 argDocCommentLine = do string "|||"

169 many (satisfy isSpace)

173 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/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)

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

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

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

8+ g x = id

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

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+