c9d2027 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+3−2

compare with master

unifiedsplit

@@ -1514,14 +1514,15 @@ data SyntaxInfo = Syn { using :: [Using],

1514 maxline :: Maybe Int,

1515 mut_nesting :: Int,

1516 dsl_info :: DSL,

1517− syn_in_quasiquote :: Int }

1517+ syn_in_quasiquote :: Int,

1518+ syn_toplevel :: Bool }

1518 deriving Show

1519 deriving Show

1519{-!

1520{-!

1520deriving instance NFData SyntaxInfo

1521deriving instance NFData SyntaxInfo

1521deriving instance Binary SyntaxInfo

1522deriving instance Binary SyntaxInfo

1522!-}

1523!-}

1523

1524

1524−defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0

1525+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True

1525

1526

1526expandNS :: SyntaxInfo -> Name -> Name

1527expandNS :: SyntaxInfo -> Name -> Name

1527expandNS syn n@(NS _ _) = n

1528expandNS syn n@(NS _ _) = n

src/Idris/Core/TT.hs+3−2

@@ -645,8 +645,9 @@ deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)

645

646updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

647updateDef n f ctxt

648− = let ds = lookupCtxtName n ctxt in

648+ = case lookupCtxtExact n ctxt of

649− foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds

649+ Just t -> addDef n (f t) ctxt

650+ Nothing -> ctxt

650

651

651toAlist :: Ctxt a -> [(Name, a)]

652toAlist :: Ctxt a -> [(Name, a)]

652toAlist ctxt = let allns = map snd (Map.toList ctxt) in

653toAlist ctxt = let allns = map snd (Map.toList ctxt) in

src/Idris/DeepSeq.hs+2−2

@@ -681,13 +681,13 @@ instance NFData Using where

681 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

682

683instance NFData SyntaxInfo where

684− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

684+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

685 = rnf x1 `seq`

686 rnf x2 `seq`

687 rnf x3 `seq`

688 rnf x4 `seq`

689 rnf x5 `seq`

690− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

690+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()

691

692instance NFData OutputMode where

693 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong

src/Idris/Delaborate.hs+1−1

@@ -488,7 +488,7 @@ pprintErr' i (ReflectionError parts orig) =

488 else empty

489pprintErr' i (ReflectionFailed msg err) =

490 text "When attempting to perform error reflection, the following internal error occurred:" <>

491− indented (pprintErr' i err) <>

491+ indented (pprintErr' i err) <+> text msg <+>

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

493pprintErr' i (ElabScriptDebug msg tm holes) =

494 text "Elaboration halted." <>

src/Idris/Directives.hs+11−2

@@ -29,8 +29,10 @@ directiveAction (DFlag cgn flag) = do

29directiveAction (DInclude cgn hdr) = do addHdr cgn hdr

30 addIBC (IBCHeader cgn hdr)

31

32+directiveAction (DHide n') = do i <- getIState

33+ ns <- allNamespaces n'

32−directiveAction (DHide n) = do setAccessibility n Hidden

34+ mapM_ (\n -> do setAccessibility n Hidden

33− addIBC (IBCAccess n Hidden)

35+ addIBC (IBCAccess n Hidden)) ns

34

36

35directiveAction (DFreeze n) = do setAccessibility n Frozen

37directiveAction (DFreeze n) = do setAccessibility n Frozen

36 addIBC (IBCAccess n Frozen)

38 addIBC (IBCAccess n Frozen)

@@ -80,3 +82,10 @@ disambiguate n = do i <- getIState

80 [(n', _)] -> return n'

82 [(n', _)] -> return n'

81 [] -> throwError (NoSuchVariable n)

83 [] -> throwError (NoSuchVariable n)

82 more -> throwError (CantResolveAlts (map fst more))

84 more -> throwError (CantResolveAlts (map fst more))

85+

86+allNamespaces :: Name -> Idris [Name]

87+allNamespaces n = do i <- getIState

88+ case lookupCtxtName n (idris_implicits i) of

89+ [(n', _)] -> return [n']

90+ [] -> throwError (NoSuchVariable n)

91+ more -> return (map fst more)

src/Idris/IBC.hs+2−2

@@ -1461,7 +1461,7 @@ instance Binary Using where

1461 _ -> error "Corrupted binary data for Using"

1462

1463instance Binary SyntaxInfo where

1464− put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

1464+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _)

1465 = do put x1

1466 put x2

1467 put x3

@@ -1477,7 +1477,7 @@ instance Binary SyntaxInfo where

1477 x5 <- get

1478 x6 <- get

1479 x7 <- get

1480− return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

1480+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True)

1481

1482instance (Binary t) => Binary (PClause' t) where

1483 put x

src/Idris/Parser.hs+4−2

@@ -608,7 +608,9 @@ fnDecl' syn = checkFixity $

608 return (doc, argDocs, fc, opts', n, nfc, acc))

609 ty <- typeExpr (allowImp syn)

610 terminator

611+ -- If it's a top level function, note the accessibility

612+ -- rules

611− addAcc n acc

613+ when (syn_toplevel syn) $ addAcc n acc

612 return (PTy doc argDocs syn fc opts' n nfc ty)

614 return (PTy doc argDocs syn fc opts' n nfc ty)

613 <|> postulate syn

615 <|> postulate syn

614 <|> caf syn

616 <|> caf syn

@@ -1125,7 +1127,7 @@ clause syn

1125 Nothing -> fail "Invalid clause"

1127 Nothing -> fail "Invalid clause"

1126 (do r <- rhs syn n

1128 (do r <- rhs syn n

1127 let ctxt = tt_ctxt ist

1129 let ctxt = tt_ctxt ist

1128− let wsyn = syn { syn_namespace = [] }

1130+ let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1129 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1131 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1130 popIndent

1132 popIndent

1131 return x,

1133 return x,