ab32c46 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitab32c466955303bf7a00be9e034c0fe3ba1eea40 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Dec 2014, 18:02 (12 years ago) parent02a36ad 9702474

2 files changed+90−94

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+76−81 src/Idris/REPL.hs+14−13

src/Idris/AbsSyntaxTree.hs+76−81

@@ -1276,8 +1276,10 @@ pprintPTerm :: PPOption -- ^^ pretty printing options

12761276 -> [FixDecl] -- ^^ Fixity declarations

12771277 -> PTerm -- ^^ the term to pretty-print

12781278 -> Doc OutputAnnotation

1279−pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1279+pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

12801280 where

1281+ startPrec = 0

1282+ funcAppPrec = 10

12811283 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

12821284 prettySe p bnd (PQuote r) =

12831285 text "![" <> pretty r <> text "]"

@@ -1287,21 +1289,21 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12871289 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

12881290 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

12891291 prettySe p bnd (PLam fc n ty sc) =

1290− bracket p 2 . group . align . hang 2 $

1292+ bracket p startPrec . group . align . hang 2 $

12911293 text "\\" <> bindingOf n False <+> text "=>" <$>

1292− prettySe 10 ((n, False):bnd) sc

1294+ prettySe startPrec ((n, False):bnd) sc

12931295 prettySe p bnd (PLet fc n ty v sc) =

1294− bracket p 2 . group . align $

1295− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>

1296− kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)

1296+ bracket p startPrec . group . align $

1297+ kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

1298+ kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

12971299 prettySe p bnd (PPi (Exp l s _) n ty sc)

12981300 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1299− bracket p 2 . group $

1300− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1301− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1301+ bracket p startPrec . group $

1302+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

1303+ st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc

13021304 | otherwise =

1303− bracket p 2 . group $

1304− group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1305+ bracket p startPrec . group $

1306+ group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)

13051307 where

13061308 st =

13071309 case s of

@@ -1309,22 +1311,22 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13091311 _ -> empty

13101312 prettySe p bnd (PPi (Imp l s _) n ty sc)

13111313 | ppopt_impl ppo =

1312− bracket p 2 $

1313− lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1314− st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1315− | otherwise = prettySe 10 ((n, True):bnd) sc

1314+ bracket p startPrec $

1315+ lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1316+ st <> text "->" </> prettySe startPrec ((n, True):bnd) sc

1317+ | otherwise = prettySe startPrec ((n, True):bnd) sc

13161318 where

13171319 st =

13181320 case s of

13191321 Static -> text "[static]" <> space

13201322 _ -> empty

13211323 prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1322− bracket p 2 $

1323− prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1324+ bracket p startPrec $

1325+ prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc

13241326 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1325− bracket p 2 $

1326− lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1327− rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1327+ bracket p startPrec $

1328+ lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>

1329+ rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc

13281330 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

13291331 | UN nm <- basename f

13301332 , not (ppopt_impl ppo) && null (getShowArgs args) =

@@ -1337,50 +1339,48 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13371339 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

13381340 case getShowArgs args of

13391341 [] -> opName True

1340− [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))

1341− [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1342+ [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1343+ [l,r] -> let precedence = maybe (startPrec - 1) prec f

13421344 in bracket p precedence $ inFix (getTm l) (getTm r)

13431345 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1344− bracket p 1 $

1346+ bracket p funcAppPrec $

13451347 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

13461348 align (group (vsep (map (prettyArgS bnd) rest)))

13471349 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

13481350 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

13491351 f = getFixity (opStr op)

1350− left l = case f of

1351− Nothing -> prettySe (-1) bnd l

1352− Just (Infixl p') -> prettySe p' bnd l

1353− Just f' -> prettySe (prec f'-1) bnd l

1354− right r = case f of

1355− Nothing -> prettySe (-1) bnd r

1356− Just (Infixr p') -> prettySe p' bnd r

1357− Just f' -> prettySe (prec f'-1) bnd r

1352+ left = case f of

1353+ Nothing -> funcAppPrec + 1

1354+ Just (Infixl p') -> p'

1355+ Just f' -> prec f' + 1

1356+ right = case f of

1357+ Nothing -> funcAppPrec + 1

1358+ Just (Infixr p') -> p'

1359+ Just f' -> prec f' + 1

13581360 inFix l r = align . group $

1359− (left l <+> opName False) <$> group (right r)

1361+ (prettySe left bnd l <+> opName False) <$>

1362+ group (prettySe right bnd r)

13601363 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

13611364 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

13621365 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1363− char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1366+ char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))

13641367 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

13651368 let args = getShowArgs as

1366− fp = prettySe 1 bnd f

1369+ fp = prettySe (startPrec + 1) bnd f

1370+ shownArgs = if ppopt_impl ppo then as else args

13671371 in

1368− bracket p 1 . group $

1369− if ppopt_impl ppo

1370− then if null as

1371− then fp

1372− else fp <+> align (vsep (map (prettyArgS bnd) as))

1373− else if null args

1374− then fp

1375− else fp <+> align (vsep (map (prettyArgS bnd) args))

1372+ bracket p funcAppPrec . group $

1373+ if null shownArgs

1374+ then fp

1375+ else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))

13761376 prettySe p bnd (PCase _ scr cases) =

1377− align $ kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <$>

1377+ align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

13781378 indent 2 (vsep (map ppcase cases))

13791379 where

1380− ppcase (l, r) = nest nestingSize $

1381− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) l <+>

1382− text "=>" <+>

1383− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) r

1380+ ppcase (l, r) = let prettyCase = prettySe startPrec

1381+ ([(n, False) | n <- vars l] ++ bnd)

1382+ in nest nestingSize $

1383+ prettyCase l <+> text "=>" <+> prettyCase r

13841384 -- Warning: this is a bit of a hack. At this stage, we don't have the

13851385 -- global context, so we can't determine which names are constructors,

13861386 -- which are types, and which are pattern variables on the LHS of the

@@ -1395,7 +1395,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13951395 noNS (NS _ _) = False

13961396 noNS _ = True

13971397

1398− prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1398+ prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

13991399 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

14001400 prettySe p bnd (PResolveTC _) = text "resolvetc"

14011401 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

@@ -1403,7 +1403,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

14031403 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

14041404 prettySe p bnd (PEq _ lt rt l r)

14051405 | ppopt_impl ppo =

1406− bracket p 1 $

1406+ bracket p eqPrec $

14071407 enclose lparen rparen eq <+>

14081408 align (group (vsep (map (prettyArgS bnd)

14091409 [PImp 0 False [] (sUN "A") lt,

@@ -1411,47 +1411,42 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

14111411 PExp 0 [] (sUN "x") l,

14121412 PExp 0 [] (sUN "y") r])))

14131413 | otherwise =

1414− bracket p 2 . align . group $

1415− prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1414+ bracket p eqPrec . align . group $

1415+ prettyTerm l <+> eq <$> group (prettyTerm r)

14161416 where eq = annName eqTy (text "=")

1417+ eqPrec = startPrec

1418+ prettyTerm = prettySe (eqPrec + 1) bnd

14171419 prettySe p bnd (PRewrite _ l r _) =

1418− bracket p 2 $

1419− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1420+ bracket p startPrec $

1421+ text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r

14201422 prettySe p bnd (PTyped l r) =

1421− lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1423+ lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen

14221424 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser

14231425 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .

14241426 align . group . vsep . punctuate (ann comma) $

1425− map (prettySe 10 bnd) elts

1427+ map (prettySe startPrec bnd) elts

14261428 where ann = case pun of

14271429 TypeOrTerm -> id

14281430 IsType -> annName pairTy

14291431 IsTerm -> annName pairCon

1430− prettySe p bnd (PDPair _ TypeOrTerm l t r) =

1431− lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1432− prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1433− annName sigmaTy lparen <>

1434− bindingOf n False <+>

1435− annName sigmaTy (text "**") <+>

1436− prettySe 10 ((n, False):bnd) r <>

1437− annName sigmaTy rparen

1438− prettySe p bnd (PDPair _ IsType l t r) =

1439− annName sigmaTy lparen <>

1440− prettySe 10 bnd l <+>

1441− annName sigmaTy (text "**") <+>

1442− prettySe 10 bnd r <>

1443− annName sigmaTy rparen

1444− prettySe p bnd (PDPair _ IsTerm l t r) =

1445− annName existsCon lparen <>

1446− prettySe 10 bnd l <+>

1447− annName existsCon (text "**") <+>

1448− prettySe 10 bnd r <>

1449− annName existsCon rparen

1432+ prettySe p bnd (PDPair _ pun l t r) =

1433+ annotated lparen <>

1434+ left <+>

1435+ annotated (text "**") <+>

1436+ prettySe startPrec (addBinding bnd) r <>

1437+ annotated rparen

1438+ where annotated = case pun of

1439+ IsType -> annName sigmaTy

1440+ IsTerm -> annName existsCon

1441+ TypeOrTerm -> id

1442+ (left, addBinding) = case (l, pun) of

1443+ (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))

1444+ _ -> (prettySe startPrec bnd l, id )

14501445 prettySe p bnd (PAlternative a as) =

14511446 lparen <> text "|" <> prettyAs <> text "|" <> rparen

14521447 where

14531448 prettyAs =

1454− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1449+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

14551450 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

14561451 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

14571452 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

@@ -1479,10 +1474,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

14791474 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

14801475 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

14811476

1482− prettyArgSe bnd arg = prettySe 0 bnd arg

1483− prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1484− prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1485− prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1477+ prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg

1478+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace

1479+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace

1480+ prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace

14861481

14871482 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

14881483 annName n = annotate (AnnName n Nothing Nothing Nothing)

@@ -1539,7 +1534,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

15391534 snat _ _ = Nothing

15401535

15411536 bracket outer inner doc

1542− | inner > outer = lparen <> doc <> rparen

1537+ | outer > inner = lparen <> doc <> rparen

15431538 | otherwise = doc

15441539

15451540 kwd = annotate AnnKeyword . text

src/Idris/REPL.hs+14−13

@@ -309,8 +309,8 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

309309 clearErr

310310 putIState (orig { idris_options = idris_options i,

311311 idris_outputmode = (IdeSlave id h) })

312− loadInputs [filename] toline

313− isetPrompt (mkPrompt [filename])

312+ mods <- loadInputs [filename] toline

313+ isetPrompt (mkPrompt mods)

314314 -- Report either success or failure

315315 i <- getIState

316316 case (errSpan i) of

@@ -321,7 +321,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

321321 (idris_parsedSpan i)

322322 in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

323323 Just x -> iPrintError $ "didn't load " ++ filename

324− ideslave h orig [filename]

324+ ideslave h orig mods

325325runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =

326326 case splitName name of

327327 Left err -> iPrintError err

@@ -622,14 +622,14 @@ processInput cmd orig inputs

622622 }

623623 clearErr

624624 mods <- loadInputs inputs Nothing

625− return (Just inputs)

625+ return (Just mods)

626626 Success (Right (Load f toline)) ->

627627 do putIState orig { idris_options = idris_options i

628628 , idris_colourTheme = idris_colourTheme i

629629 }

630630 clearErr

631631 mod <- loadInputs [f] toline

632− return (Just [f])

632+ return (Just mod)

633633 Success (Right (ModImport f)) ->

634634 do clearErr

635635 fmod <- loadModule f

@@ -1334,7 +1334,7 @@ idris opts = do res <- runExceptT $ execStateT totalMain idrisInit

13341334 [] -> return ()

13351335

13361336

1337−loadInputs :: [FilePath] -> Maybe Int -> Idris ()

1337+loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

13381338loadInputs inputs toline -- furthest line to read in input source files

13391339 = idrisCatch

13401340 (do ist <- getIState

@@ -1363,7 +1363,7 @@ loadInputs inputs toline -- furthest line to read in input source files

13631363 when (not (all ibc ifiles) || loadCode) $

13641364 tryLoad False (filter (not . ibc) ifiles)

13651365 -- return the files that need rechecking

1366− return ifiles)

1366+ return (input, ifiles))

13671367 ninputs

13681368 inew <- getIState

13691369 let tidata = idris_tyinfodata inew

@@ -1372,7 +1372,7 @@ loadInputs inputs toline -- furthest line to read in input source files

13721372 case errSpan inew of

13731373 Nothing ->

13741374 do putIState (ist { idris_tyinfodata = tidata })

1375− ibcfiles <- mapM findNewIBC (nub (concat ifiles))

1375+ ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

13761376 tryLoad True (mapMaybe id ibcfiles)

13771377 _ -> return ()

13781378 ist <- getIState

@@ -1383,7 +1383,7 @@ loadInputs inputs toline -- furthest line to read in input source files

13831383 [] -> performUsageAnalysis -- interactive

13841384 _ -> return [] -- batch, will be checked by the compiler

13851385

1386− return ())

1386+ return (map fst ifiles))

13871387 (\e -> do i <- getIState

13881388 case e of

13891389 At f e' -> do setErrSpan f

@@ -1392,7 +1392,8 @@ loadInputs inputs toline -- furthest line to read in input source files

13921392 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

13931393 -- Issue #1576 on the issue tracker.

13941394 -- https://github.com/idris-lang/Idris-dev/issues/1576

1395− iWarn emptyFC $ pprintErr i e)

1395+ iWarn emptyFC $ pprintErr i e

1396+ return [])

13961397 where -- load all files, stop if any fail

13971398 tryLoad :: Bool -> [IFileType] -> Idris ()

13981399 tryLoad keepstate [] = warnTotality >> return ()

@@ -1538,7 +1539,7 @@ idrisMain opts =

15381539 iputStrLn banner

15391540

15401541 orig <- getIState

1541− when (not idesl) $ loadInputs inputs Nothing

1542+ mods <- if idesl then return [] else loadInputs inputs Nothing

15421543

15431544 runIO $ hSetBuffering stdout LineBuffering

15441545

@@ -1580,8 +1581,8 @@ idrisMain opts =

15801581

15811582 when (runrepl && not idesl) $ do

15821583-- clearOrigPats

1583− startServer port orig inputs

1584− runInputT (replSettings (Just historyFile)) $ repl orig inputs

1584+ startServer port orig mods

1585+ runInputT (replSettings (Just historyFile)) $ repl orig mods

15851586 let idesock = IdeslaveSocket `elem` opts

15861587 when (idesl) $ ideslaveStart idesock orig inputs

15871588 ok <- noErrors