a85feeb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

a85feebEdwin Brady13 years ago

CHANGELOG+3

compare with master

unifiedsplit

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

3* IDE support for retrieving structured information about metavariables

4* Experimental Bits support for JavaScript

5* 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.

7Internal changes

10Internal changes

main/Main.hs+1

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

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

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

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

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+54−13

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

357 | OutputTy OutputType

358 | Extension LanguageExt

359 | InterpretScript String

360+ | EvalExpr String

360 | TargetTriple String

361 | TargetTriple String

361 | TargetCPU String

362 | TargetCPU String

362 | OptLevel Word

363 | OptLevel Word

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

986 falseTy, pairTy, pairCon,

987 falseTy, pairTy, pairCon,

987 eqTy, eqCon, inferTy, inferCon]

988 eqTy, eqCon, inferTy, inferCon]

988

989

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

989unitTy = sMN 0 "__Unit"

991unitTy = sMN 0 "__Unit"

990unitCon = sMN 0 "__II"

992unitCon = sMN 0 "__II"

991unitDecl = PDatadecl unitTy PType

993unitDecl = PDatadecl unitTy PType

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

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

993unitOpts = [DefaultEliminator]

995unitOpts = [DefaultEliminator]

994

996

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

995falseTy = sMN 0 "__False"

1002falseTy = sMN 0 "__False"

996falseDecl = PDatadecl falseTy PType []

1003falseDecl = PDatadecl falseTy PType []

997falseOpts = []

1004falseOpts = []

998

1005

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

999pairTy = sMN 0 "__Pair"

1007pairTy = sMN 0 "__Pair"

1000pairCon = sMN 0 "__MkPair"

1008pairCon = sMN 0 "__MkPair"

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

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

1010+ [(pairConDoc, pairConParamDoc,

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

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

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

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

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

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

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

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

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

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

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

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

1008 where n a = sMN 0 a

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

1009pairOpts = []

1021pairOpts = []

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

1010

1025

1011eqTy = sUN "="

1026eqTy = sUN "="

1012eqCon = sUN "refl"

1027eqCon = 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+

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

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

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

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

1015 PType)

1044 PType)

1045+ [(reflDoc, reflParamDoc,

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

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

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

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

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

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

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

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

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

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

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

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

1022 where n a = sMN 0 a

1052 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+

1023eqOpts = []

1064eqOpts = []

1024

1065

1025elimName = sUN "__Elim"

1066elimName = sUN "__Elim"

src/Idris/Completion.hs+1

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

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

161 completeArg OptionArg = completeOption (prev, next)

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

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

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

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

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

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

165 completeArg ColourArg = completeColour (prev, next)

166 completeArg ColourArg = completeColour (prev, next)

src/Idris/Docstrings.hs+1−1

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

69renderInline :: CT.Inline -> Doc OutputAnnotation

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

71−renderInline CT.Space = space

71+renderInline CT.Space = softline

72renderInline CT.SoftBreak = softline

73renderInline CT.LineBreak = line

74renderInline (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

605

606elabPrims :: Idris ()

607elabPrims = do mapM_ (elabDecl EAll toplevel)

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

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

609− (zip

609+ (zip4

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

612 addNameHint eqTy (sUN "prf")

614 addNameHint eqTy (sUN "prf")

613 elabDecl EAll toplevel elimDecl

615 elabDecl EAll toplevel elimDecl

614 mapM_ elabPrim primitives

616 mapM_ elabPrim primitives

src/Idris/REPL.hs+29−2

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

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

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

1202parseArgs ("--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

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

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

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

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

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

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

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

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

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

1369 runIO $ exitWith (ExitFailure 1)

1371 runIO $ exitWith (ExitFailure 1)

1370 [expr] -> return (Just expr)

1372 [expr] -> return (Just expr)

1373+ let immediate = opt getEvalExpr opts

1374+

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

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

1372 putIState (i { default_total = True })

1376 putIState (i { default_total = True })

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

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

1374 when (not runrepl) $ setWidth InfinitelyWide

1378 when (not runrepl) $ setWidth InfinitelyWide

1375 mapM_ addLangExt (opt getLanguageExt opts)

1379 mapM_ addLangExt (opt getLanguageExt opts)

1376 setREPL runrepl

1380 setREPL runrepl

1377− setQuiet (quiet || isJust script)

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

1378 setIdeSlave idesl

1382 setIdeSlave idesl

1379 setVerbose verbose

1383 setVerbose verbose

1380 setCmdLine opts

1384 setCmdLine opts

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

1402 return ()

1406 return ()

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

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

1404 return ()

1408 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

1406

1416

1407 orig <- getIState

1417 orig <- getIState

1408 loadInputs stdout inputs

1418 loadInputs stdout inputs

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

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

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

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

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

1420

1430

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+

1421 case script of

1444 case script of

1422 Nothing -> return ()

1445 Nothing -> return ()

1423 Just expr -> execScript expr

1446 Just expr -> execScript expr

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

1554getExecScript (InterpretScript expr) = Just expr

1577getExecScript (InterpretScript expr) = Just expr

1555getExecScript _ = Nothing

1578getExecScript _ = Nothing

1556

1579

1580+getEvalExpr :: Opt -> Maybe String

1581+getEvalExpr (EvalExpr expr) = Just expr

1582+getEvalExpr _ = Nothing

1583+

1557getOutputTy :: Opt -> Maybe OutputType

1584getOutputTy :: Opt -> Maybe OutputType

1558getOutputTy (OutputTy t) = Just t

1585getOutputTy (OutputTy t) = Just t

1559getOutputTy _ = Nothing

1586getOutputTy _ = Nothing

test/reg041/expected+1−2

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

1Type 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)

test/reg041/run+1−1

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

1#!/usr/bin/env bash

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

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

3idris $@ showu.idr -o reg040

4./reg040

5rm -f reg040 *.ibc