a85feeb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commita85feeb7b27a573f63d8e5117f73f1ca0e99377a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 21 Apr 2014, 16:38 (13 years ago) parent0bd42f1 03a24ff

9 files changed+96−22

compare with master

unifiedsplit

CHANGELOG+3 main/Main.hs+1 src/Idris/AbsSyntaxTree.hs+54−13 src/Idris/Completion.hs+1 src/Idris/Docstrings.hs+1−1 src/Idris/ElabDecls.hs+5−3 src/Idris/REPL.hs+29−2 test/reg041/expected+1−2 test/reg041/run+1−1

CHANGELOG+3

@@ -3,6 +3,9 @@ New in 0.9.13:

33* IDE support for retrieving structured information about metavariables

44* Experimental Bits support for JavaScript

55* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator

6+* Command line option -e (or --eval) to evaluate expressions without loading the

7+ REPL. This is useful for writing more portable tests.

8+* Many more of the basic functions and datatypes are documented.

710Internal changes

811

main/Main.hs+1

@@ -100,6 +100,7 @@ usagemsg = usagemsghdr ++ "\n" ++

100100 "\t --clean IPKG Clean package\n" ++

101101 "\t --build IPKG Build package\n" ++

102102 "\t --mkdoc IPKG Generate IdrisDoc for package\n" ++

103+ "\t -e --eval EXPR Evaluate an expression without loading the REPL" ++

103104 "\t --exec EXPR Execute as idris\n" ++

104105 "\t --libdir Display library directory\n" ++

105106 "\t --link Display link directory\n" ++

src/Idris/AbsSyntaxTree.hs+54−13

@@ -357,6 +357,7 @@ data Opt = Filename String

357357 | OutputTy OutputType

358358 | Extension LanguageExt

359359 | InterpretScript String

360+ | EvalExpr String

360361 | TargetTriple String

361362 | TargetCPU String

362363 | OptLevel Word

@@ -986,40 +987,80 @@ primNames = [unitTy, unitCon,

986987 falseTy, pairTy, pairCon,

987988 eqTy, eqCon, inferTy, inferCon]

988989

990+unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."

989991unitTy = sMN 0 "__Unit"

990992unitCon = sMN 0 "__II"

991993unitDecl = PDatadecl unitTy PType

992− [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]

994+ [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]

993995unitOpts = [DefaultEliminator]

994996

997+falseDoc = parseDocstring . T.pack $

998+ "The empty type, also known as the trivially false proposition." ++

999+ "\n\n" ++

1000+ "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++

1001+ "of type `_|_` in scope."

9951002falseTy = sMN 0 "__False"

9961003falseDecl = PDatadecl falseTy PType []

9971004falseOpts = []

9981005

1006+pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."

9991007pairTy = sMN 0 "__Pair"

10001008pairCon = sMN 0 "__MkPair"

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

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

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

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

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

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

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

1010+ [(pairConDoc, pairConParamDoc,

1011+ pairCon, PPi impl (n "A") PType (

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

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

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

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

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

10081017 where n a = sMN 0 a

1018+ pairConDoc = parseDocstring . T.pack $ "A pair of elements"

1019+ pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),

1020+ (n "b", parseDocstring . T.pack $ "the right element of the pair")]

10091021pairOpts = []

1022+pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),

1023+ (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]

1024+ where n a = sMN 0 a

10101025

10111026eqTy = sUN "="

10121027eqCon = sUN "refl"

1028+eqDoc = parseDocstring . T.pack $

1029+ "The propositional equality type. A proof that `x` = `y`." ++

1030+ "\n\n" ++

1031+ "To use such a proof, pattern-match on it, and the two equal things will " ++

1032+ "then need to be the _same_ pattern." ++

1033+ "\n\n" ++

1034+ "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++

1035+ "is possible to state equalities between values of potentially different " ++

1036+ "types. This is sometimes referred to in the literature as \"John Major\" " ++

1037+ "equality." ++

1038+ "\n\n" ++

1039+ "Thus, if Idris can't infer the type of one side of the equality, then " ++

1040+ "you may need to annotate it. See the function `the`."

1041+

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

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

10151044 PType)

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

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

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

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

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

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

1045+ [(reflDoc, reflParamDoc,

1046+ eqCon, PPi impl (n "A") PType (

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

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

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

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

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

10221052 where n a = sMN 0 a

1053+ reflDoc = parseDocstring . T.pack $

1054+ "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1055+ "shown that both sides are in fact equal."

1056+ reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),

1057+ (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]

1058+

1059+eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),

1060+ (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")

1061+ ]

1062+ where n a = sMN 0 a

1063+

10231064eqOpts = []

10241065

10251066elimName = sUN "__Elim"

src/Idris/Completion.hs+1

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

160160 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name

161161 completeArg OptionArg = completeOption (prev, next)

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

163+ completeArg NamespaceArg = noCompletion (prev, next) -- FIXME do later

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

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

165166 completeArg ColourArg = completeColour (prev, next)

src/Idris/Docstrings.hs+1−1

@@ -68,7 +68,7 @@ renderInlines = F.foldr (<>) empty . fmap renderInline

6868

6969renderInline :: CT.Inline -> Doc OutputAnnotation

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

71−renderInline CT.Space = space

71+renderInline CT.Space = softline

7272renderInline CT.SoftBreak = softline

7373renderInline CT.LineBreak = line

7474renderInline (CT.Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines txt -- TODO

src/Idris/ElabDecls.hs+5−3

@@ -605,10 +605,12 @@ elabEliminator paramPos n ty cons info = do

605605

606606elabPrims :: Idris ()

607607elabPrims = do mapM_ (elabDecl EAll toplevel)

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

609− (zip

608+ (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)

609+ (zip4

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

611− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

611+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]

612+ [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]

613+ [[], [], [], pairParamDoc, eqParamDoc]))

612614 addNameHint eqTy (sUN "prf")

613615 elabDecl EAll toplevel elimDecl

614616 mapM_ elabPrim primitives

src/Idris/REPL.hs+29−2

@@ -1200,6 +1200,8 @@ parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

12001200parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

12011201parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

12021202parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

1203+parseArgs ("--eval":expr:ns) = EvalExpr expr : parseArgs ns

1204+parseArgs ("-e":expr:ns) = EvalExpr expr : parseArgs ns

12031205parseArgs ["--exec"] = InterpretScript "Main.main" : []

12041206parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

12051207parseArgs (('-':'X':extName):ns) = case maybeRead extName of

@@ -1368,13 +1370,15 @@ idrisMain opts =

13681370 x:y:xs -> do iputStrLn "More than one interpreter expression found."

13691371 runIO $ exitWith (ExitFailure 1)

13701372 [expr] -> return (Just expr)

1373+ let immediate = opt getEvalExpr opts

1374+

13711375 when (DefaultTotal `elem` opts) $ do i <- getIState

13721376 putIState (i { default_total = True })

13731377 setColourise $ not quiet && last (True : opt getColour opts)

13741378 when (not runrepl) $ setWidth InfinitelyWide

13751379 mapM_ addLangExt (opt getLanguageExt opts)

13761380 setREPL runrepl

1377− setQuiet (quiet || isJust script)

1381+ setQuiet (quiet || isJust script || not (null immediate))

13781382 setIdeSlave idesl

13791383 setVerbose verbose

13801384 setCmdLine opts

@@ -1402,7 +1406,13 @@ idrisMain opts =

14021406 return ()

14031407 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

14041408 return ()

1405− when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner

1409+ when (runrepl &&

1410+ not quiet &&

1411+ not idesl &&

1412+ not (isJust script) &&

1413+ not nobanner &&

1414+ null immediate) $

1415+ iputStrLn banner

14061416

14071417 orig <- getIState

14081418 loadInputs stdout inputs

@@ -1418,6 +1428,19 @@ idrisMain opts =

14181428 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

14191429 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

14201430

1431+ case immediate of

1432+ [] -> return ()

1433+ exprs -> do setWidth InfinitelyWide

1434+ mapM_ (\str -> do ist <- getIState

1435+ c <- colourise

1436+ case parseExpr ist str of

1437+ Failure err -> do iputStrLn $ show (fixColour c err)

1438+ runIO $ exitWith (ExitFailure 1)

1439+ Success e -> process stdout "" (Eval e))

1440+ exprs

1441+ runIO $ exitWith ExitSuccess

1442+

1443+

14211444 case script of

14221445 Nothing -> return ()

14231446 Just expr -> execScript expr

@@ -1554,6 +1577,10 @@ getExecScript :: Opt -> Maybe String

15541577getExecScript (InterpretScript expr) = Just expr

15551578getExecScript _ = Nothing

15561579

1580+getEvalExpr :: Opt -> Maybe String

1581+getEvalExpr (EvalExpr expr) = Just expr

1582+getEvalExpr _ = Nothing

1583+

15571584getOutputTy :: Opt -> Maybe OutputType

15581585getOutputTy (OutputTy t) = Just t

15591586getOutputTy _ = Nothing

test/reg041/expected+1−2

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

11Type checking ./ott.idr

2−?prf : (x : Bool) ->

3−(x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)

2+?prf : (x : Bool) -> (x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)

43Z

test/reg041/run+1−1

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

11#!/usr/bin/env bash

2−echo "example" | idris $@ --quiet ott.idr

2+idris $@ --quiet ott.idr -e example

33idris $@ showu.idr -o reg040

44./reg040

55rm -f reg040 *.ibc