git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master'
commit29a1e77884f6fabd97a00d79570557286858c4a7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 10 Mar 2014, 08:59 (13 years ago) parent756b44fa7e6550
26 files changed+445−129
compare with master
unifiedsplit
CHANGELOG+12−9 Makefile+1−1 idris.cabal+2 libs/neweffects/Effects.idr+7−2 src/IRTS/CodegenJavaScript.hs+7−4 src/Idris/AbsSyntax.hs+8−1 src/Idris/AbsSyntaxTree.hs+33−29 src/Idris/Completion.hs+5−1 src/Idris/DSL.hs+2−2 src/Idris/DeepSeq.hs+43−1 src/Idris/Docs.hs+15−13 src/Idris/Docstrings.hs+80 src/Idris/ElabDecls.hs+30−27 src/Idris/IBC.hs+93−8 src/Idris/ParseData.hs+8−6 src/Idris/ParseExpr.hs+25−6 src/Idris/ParseHelpers.hs+14−9 src/Idris/ParseOps.hs−1 src/Idris/Parser.hs+7−5 src/Idris/Prover.hs+2−1 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+1 test/Makefile+3−3 test/sugar004/expected+3 test/sugar004/run+6 test/sugar004/sugar004.idr+36
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+2
@@ -440,6 +440,7 @@ Library
440440 , Idris.DeepSeq
441441 , Idris.Delaborate
442442 , Idris.Docs
443+ , Idris.Docstrings
443444 , Idris.ElabDecls
444445 , Idris.ElabTerm
445446 , Idris.Error
@@ -506,6 +507,7 @@ Library
506507 , ansi-wl-pprint
507508 , binary
508509 , bytestring
510+ , cheapskate
509511 , containers >= 0.5
510512 , directory
511513 , directory >= 1.2
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+8−1
@@ -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
src/Idris/AbsSyntaxTree.hs+33−29
@@ -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
@@ -336,6 +339,7 @@ data Opt = Filename String
336339 | Client String
337340 | ShowOrigErr
338341 | AutoWidth -- ^ Automatically adjust terminal width
342+ | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
339343 deriving (Show, Eq)
340344
341345-- Parsed declarations
@@ -450,15 +454,15 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms
450454-- datatypes and typeclasses.
451455data PDecl' t
452456 = PFix FC Fixity [String] -- ^ Fixity declaration
453− | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
454− | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
457+ | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
458+ | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
455459 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
456460 | PCAF FC Name t -- ^ Top level constant
457− | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
461+ | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
458462 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
459463 | PNamespace String [PDecl' t] -- ^ New namespace
460− | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
461− | PClass String SyntaxInfo FC
464+ | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration
465+ | PClass Docstring SyntaxInfo FC
462466 [t] -- constraints
463467 Name
464468 [(Name, t)] -- parameters
@@ -512,7 +516,7 @@ deriving instance NFData PClause'
512516-- | Data declaration
513517data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
514518 d_tcon :: t, -- ^ Type constructor
515− d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors
519+ d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
516520 }
517521 -- ^ Data declaration
518522 | PLaterdecl { d_name :: Name, d_tcon :: t }
@@ -737,7 +741,7 @@ type PTactic = PTactic' PTerm
737741
738742data PDo' t = DoExp FC t
739743 | DoBind FC Name t
740− | DoBindP FC t t
744+ | DoBindP FC t t [(t,t)]
741745 | DoLet FC Name t t
742746 | DoLetP FC t t
743747 deriving (Eq, Functor)
@@ -749,7 +753,7 @@ deriving instance NFData PDo'
749753instance Sized a => Sized (PDo' a) where
750754 size (DoExp fc t) = 1 + size fc + size t
751755 size (DoBind fc nm t) = 1 + size fc + size nm + size t
752− size (DoBindP fc l r) = 1 + size fc + size l + size r
756+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
753757 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
754758 size (DoLetP fc l r) = 1 + size fc + size l + size r
755759
@@ -948,9 +952,9 @@ inferTy = sMN 0 "__Infer"
948952inferCon = sMN 0 "__infer"
949953inferDecl = PDatadecl inferTy
950954 PType
951− [("", [], inferCon, PPi impl (sMN 0 "iType") PType (
952− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
953− (PRef bi inferTy)), bi, [])]
955+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
956+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
957+ (PRef bi inferTy)), bi, [])]
954958inferOpts = []
955959
956960infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
@@ -978,7 +982,7 @@ primNames = [unitTy, unitCon,
978982unitTy = sMN 0 "__Unit"
979983unitCon = sMN 0 "__II"
980984unitDecl = PDatadecl unitTy PType
981− [("", [], unitCon, PRef bi unitTy, bi, [])]
985+ [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]
982986unitOpts = [DefaultEliminator]
983987
984988falseTy = sMN 0 "__False"
@@ -988,12 +992,12 @@ falseOpts = []
988992pairTy = sMN 0 "__Pair"
989993pairCon = sMN 0 "__MkPair"
990994pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
991− [("", [], pairCon, PPi impl (n "A") PType (
992− PPi impl (n "B") PType (
993− PPi expl (n "a") (PRef bi (n "A")) (
994− PPi expl (n "b") (PRef bi (n "B"))
995− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
996− pexp (PRef bi (n "B"))])))), bi, [])]
995+ [(emptyDocstring, [], pairCon, PPi impl (n "A") PType (
996+ PPi impl (n "B") PType (
997+ PPi expl (n "a") (PRef bi (n "A")) (
998+ PPi expl (n "b") (PRef bi (n "B"))
999+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1000+ pexp (PRef bi (n "B"))])))), bi, [])]
9971001 where n a = sMN 0 a
9981002pairOpts = []
9991003
@@ -1002,21 +1006,21 @@ eqCon = sUN "refl"
10021006eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
10031007 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
10041008 PType)
1005− [("", [], eqCon, PPi impl (n "A") PType (
1006− PPi impl (n "x") (PRef bi (n "A"))
1007− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1008− pimp (n "B") Placeholder False,
1009− pexp (PRef bi (n "x")),
1010− pexp (PRef bi (n "x"))])), bi, [])]
1009+ [(emptyDocstring, [], eqCon, PPi impl (n "A") PType (
1010+ PPi impl (n "x") (PRef bi (n "A"))
1011+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1012+ pimp (n "B") Placeholder False,
1013+ pexp (PRef bi (n "x")),
1014+ pexp (PRef bi (n "x"))])), bi, [])]
10111015 where n a = sMN 0 a
10121016eqOpts = []
10131017
10141018elimName = sUN "__Elim"
10151019elimMethElimTy = sUN "__elimTy"
10161020elimMethElim = sUN "elim"
1017−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1018− [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1019− PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1021+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1022+ [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1023+ PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
10201024
10211025-- Defined in builtins.idr
10221026sigmaTy = sUN "Exists"
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/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+30−27
@@ -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 -}
@@ -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]))
@@ -665,7 +668,7 @@ 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) []]
670673 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
671674 | otherwise ->
@@ -673,7 +676,7 @@ elabProvider info syn fc what n ty tm
673676 Postulate
674677 | what `elem` [ProvPostulate, ProvAny] ->
675678 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
677680 logLvl 3 $ "Elaborated provided postulate " ++ show n
678681 | otherwise ->
679682 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -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
@@ -1166,7 +1169,7 @@ elabPE info fc caller r =
11661169 (map (\ (lhs, rhs) ->
11671170 (showTmImpls lhs ++ " = " ++
11681171 showTmImpls rhs)) pats)
1169− elabType info defaultSyntax "" [] fc opts newnm specTy
1172+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
11701173 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
11711174 elabClauses info fc opts newnm def
11721175 logLvl 2 $ "Specialised " ++ show newnm)
@@ -1725,7 +1728,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17251728
17261729data MArgTy = IA | EA | CA deriving Show
17271730
1728−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1731+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
17291732 FC -> [PTerm] ->
17301733 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
17311734elabClass info syn doc fc constraints tn ps ds
@@ -1752,7 +1755,7 @@ elabClass info syn doc fc constraints tn ps ds
17521755 let cty = impbind ps $ conbind constraints
17531756 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
17541757 constraint
1755− let cons = [("", [], cn, cty, fc, [])]
1758+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
17561759 let ddecl = PDatadecl tn tty cons
17571760 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
17581761 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl
@@ -1807,7 +1810,7 @@ elabClass info syn doc fc constraints tn ps ds
18071810 case lookup n mtys of
18081811 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
18091812 let ds = map (decorateid defaultdec)
1810− [PTy "" [] syn fc [] n ty',
1813+ [PTy emptyDocstring [] syn fc [] n ty',
18111814 PClauses fc (o ++ opts) n cs]
18121815 iLOG (show ds)
18131816 return (n, ((defaultdec n, ds!!1), ds))
@@ -1845,7 +1848,7 @@ elabClass info syn doc fc constraints tn ps ds
18451848 addInstance False conn' cfn
18461849 addIBC (IBCInstance False conn' cfn)
18471850-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1848− return [PTy "" [] syn fc [] cfn ty,
1851+ return [PTy emptyDocstring [] syn fc [] cfn ty,
18491852 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
18501853
18511854 -- Generate a top level function which looks up a method in a given
@@ -1909,7 +1912,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19091912 let constraint = PApp fc (PRef fc n) (map pexp ps)
19101913 let iname = mkiname n ps expn
19111914 when (what /= EDefns) $ do
1912− nty <- elabType' True info syn "" [] fc [] iname t
1915+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
19131916 -- if the instance type matches any of the instances we have already,
19141917 -- and it's not a named instance, then it's overlapping, so report an error
19151918 case expn of
@@ -2061,7 +2064,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20612064 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
20622065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
20632066
2064− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t
2067+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
20652068
20662069 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
20672070 conbind [] x = x
@@ -2308,7 +2311,7 @@ inferredDiff fc inf user =
23082311-- | Check a PTerm against documentation and ensure that every documented
23092312-- argument actually exists. This must be run _after_ implicits have been
23102313-- found, or it will give spurious errors.
2311−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()
2314+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
23122315checkDocs fc args tm = cd (Map.fromList args) tm
23132316 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
23142317 cd as _ | Map.null as = return ()
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−9
@@ -1,4 +1,5 @@
11{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2+{-# LANGUAGE StandaloneDeriving #-}
23module Idris.ParseHelpers where
34
45import Prelude hiding (pi)
@@ -16,6 +17,7 @@ import Idris.AbsSyntax
1617import Idris.Core.TT
1718import Idris.Core.Evaluate
1819import Idris.Delaborate (pprintErr)
20+import Idris.Docstrings
1921
2022import qualified Util.Pretty as Pretty (text)
2123
@@ -41,7 +43,9 @@ import Debug.Trace
4143type IdrisParser = StateT IState IdrisInnerParser
4244
4345newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
44− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)
46+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing{-, Parsing-}, DeltaParsing, MarkParsing Delta, Monoid)
47+
48+deriving instance Parsing IdrisInnerParser
4549
4650instance TokenParsing IdrisInnerParser where
4751 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
@@ -139,25 +143,26 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
139143{-| Parses a documentation comment (similar to haddoc) given a marker character
140144
141145@
142− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
143− | '{ -' DocCommentMarket_t ~'- }'* '- }'
146+ DocComment_t ::= '|||' ~EOL_t* EOL_t
144147 ;
145148@
146149 -}
147−docComment :: IdrisParser (String, [(Name, String)])
150+docComment :: IdrisParser (Docstring, [(Name, Docstring)])
148151docComment = do dc <- pushIndent *> docCommentLine
149152 rest <- many (indented docCommentLine)
150153 args <- many (indented argDocCommentLine)
151154 popIndent
152− return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)
155+ return (parseDocstring $ T.pack (concat . intersperse "\n" $ dc:rest),
156+ map (\(n, d) -> (n, parseDocstring (T.pack d))) args)
153157
154158 where docCommentLine :: MonadicParsing m => m String
155159 docCommentLine = try (do string "|||"
156− many (satisfy isSpace)
157− first <- satisfy (\c -> not (isEol c || c == '@'))
158− res <- many (satisfy (not . isEol))
160+ many (satisfy (==' '))
161+ contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))
162+ res <- many (satisfy (not . isEol))
163+ return $ first:res)
159164 eol ; someSpace
160− return (first:res))-- ++ concat rest))
165+ return contents)-- ++ concat rest))
161166 <?> ""
162167 argDocCommentLine = do string "|||"
163168 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/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+