1019ce5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Source file stylings & Haddock.

1019ce5Jan de Muijnck-Hughes10 years ago

src/Idris/ASTUtils.hs+14−19

compare with master

unifiedsplit

@@ -1,6 +1,6 @@

1module Idris.ASTUtils(Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState,

2 fputState, idris_fixities, ist_callgraph, ist_optimisation,

3− known_classes, known_terms, opt_detaggable, opt_inaccessible,

3+ known_classes, known_terms, opt_detaggable, opt_inaccessible,

4 opts_idrisCmdline, repl_definitions) where

6-- This implements just a few basic lens-like concepts to ease state updates.

@@ -65,8 +65,9 @@ fputState field x = fmodifyState field (const x)

65fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()

66fmodifyState field f = modify $ fmodify field f

68−-- Exact-name context lookup; uses Nothing for deleted values (read+write!).

68+-- | Exact-name context lookup; uses Nothing for deleted values

69+-- (read+write!).

69−--

70+--

70-- Reading a non-existing value yields Nothing,

71-- Reading a non-existing value yields Nothing,

71-- writing Nothing deletes the value (if it existed).

72-- writing Nothing deletes the value (if it existed).

72ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)

73ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)

@@ -93,7 +94,7 @@ maybe_default dflt = Field (fromMaybe dflt) (const . Just)

93-- OptInfo

94-- OptInfo

94----------

95----------

96−-- the optimisation record for the given (exact) name

97+-- | the optimisation record for the given (exact) name

97ist_optimisation :: Name -> Field IState OptInfo

98ist_optimisation :: Name -> Field IState OptInfo

98ist_optimisation n =

99ist_optimisation n =

99 maybe_default Optimise

100 maybe_default Optimise

@@ -103,7 +104,7 @@ ist_optimisation n =

103 . ctxt_lookup n

104 . ctxt_lookup n

104 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

105 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

105

106

106−-- two fields of the optimisation record

107+-- | two fields of the optimisation record

107opt_inaccessible :: Field OptInfo [(Int, Name)]

108opt_inaccessible :: Field OptInfo [(Int, Name)]

108opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })

109opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })

109

110

@@ -111,10 +112,7 @@ opt_detaggable :: Field OptInfo Bool

111opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

112opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

112

113

114

114−-- CGInfo

115−---------

116−

117−-- callgraph record for the given (exact) name

115+-- | callgraph record for the given (exact) name

118ist_callgraph :: Name -> Field IState CGInfo

116ist_callgraph :: Name -> Field IState CGInfo

119ist_callgraph n =

117ist_callgraph n =

120 maybe_default CGInfo

118 maybe_default CGInfo

@@ -126,18 +124,16 @@ ist_callgraph n =

126cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

124cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

127cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

125cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

128

126

129−-- Commandline flags

127+-- | Commandline flags

130−--------------------

131−

132opts_idrisCmdline :: Field IState [Opt]

128opts_idrisCmdline :: Field IState [Opt]

133opts_idrisCmdline =

129opts_idrisCmdline =

134 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })

130 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })

135 . Field idris_options (\v ist -> ist{ idris_options = v })

131 . Field idris_options (\v ist -> ist{ idris_options = v })

136

132

137−-- TT Context

133+-- | TT Context

138−-------------

134+--

139−-- This has a terrible name, but I'm not sure of a better one that isn't

135+-- This has a terrible name, but I'm not sure of a better one that

140−-- confusingly close to tt_ctxt

136+-- isn't confusingly close to tt_ctxt

141known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))

137known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))

142known_terms = Field (definitions . tt_ctxt)

138known_terms = Field (definitions . tt_ctxt)

143 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

139 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

@@ -146,11 +142,10 @@ known_classes :: Field IState (Ctxt ClassInfo)

146known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})

142known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})

147

143

148

144

149−-- Names defined at the repl

145+-- | Names defined at the repl

150−----------------------------

151repl_definitions :: Field IState [Name]

146repl_definitions :: Field IState [Name]

152repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})

147repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})

153

148

154−-- Fixity declarations in an IState

149+-- | Fixity declarations in an IState

155idris_fixities :: Field IState [FixDecl]

150idris_fixities :: Field IState [FixDecl]

156idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})

151idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})

src/Idris/AbsSyntax.hs+40−37

@@ -145,8 +145,8 @@ addLangExt ErrorReflection = do i <- getIState

145 idris_language_extensions = ErrorReflection : idris_language_extensions i

146 }

147

148−-- Transforms are organised by the function being applied on the lhs of the

148+-- | Transforms are organised by the function being applied on the lhs

149−-- transform, to make looking up appropriate transforms quicker

149+-- of the transform, to make looking up appropriate transforms quicker

150addTrans :: Name -> (Term, Term) -> Idris ()

151addTrans basefn t

152 = do i <- getIState

@@ -331,8 +331,8 @@ isTyInferred n

331 [TIPartial] -> return True

332 _ -> return False

333

334−-- | Adds error handlers for a particular function and argument. If names are

334+-- | Adds error handlers for a particular function and argument. If

335−-- ambiguous, all matching handlers are updated.

335+-- names are ambiguous, all matching handlers are updated.

336addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

337addFunctionErrorHandlers f arg hs =

338 do i <- getIState

@@ -350,7 +350,7 @@ getFunctionErrorHandlers f arg = do i <- getIState

350 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)

351

352

353−-- Trace all the names in a call graph starting at the given name

353+-- | Trace all the names in a call graph starting at the given name

354getAllNames :: Name -> Idris [Name]

355getAllNames n = allNames [] n

356

@@ -456,12 +456,11 @@ addInstance int res n i

456 chaser (NS n _) = chaser n

457 chaser _ = False

458

459−-- Add a privileged implementation - one which instance search will happily

459+-- | Add a privileged implementation - one which instance search will

460−-- resolve immediately if it is type correct

460+-- happily resolve immediately if it is type correct This is used for

461−-- This is used for naming parent implementations when defining an

461+-- naming parent implementations when defining an implementation with

462−-- implementation with constraints.

463−-- Returns the old list, so we can revert easily at the end of a block

462+-- constraints. Returns the old list, so we can revert easily at the

464−

463+-- end of a block

465addOpenImpl :: [Name] -> Idris [Name]

464addOpenImpl :: [Name] -> Idris [Name]

466addOpenImpl ns = do ist <- getIState

465addOpenImpl ns = do ist <- getIState

467 ns' <- mapM (checkValid ist) ns

466 ns' <- mapM (checkValid ist) ns

@@ -530,7 +529,7 @@ resetNameIdx :: Idris ()

530resetNameIdx = do i <- getIState

529resetNameIdx = do i <- getIState

531 put (i { idris_nameIdx = (0, emptyContext) })

530 put (i { idris_nameIdx = (0, emptyContext) })

532

531

533−-- Used to preserve sharing of names

532+-- | Used to preserve sharing of names

534addNameIdx :: Name -> Idris (Int, Name)

533addNameIdx :: Name -> Idris (Int, Name)

535addNameIdx n = do i <- getIState

534addNameIdx n = do i <- getIState

536 let (i', x) = addNameIdx' i n

535 let (i', x) = addNameIdx' i n

@@ -597,7 +596,8 @@ withContext ctx name dflt action = do

597withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()

596withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()

598withContext_ ctx name action = withContext ctx name () action

597withContext_ ctx name action = withContext ctx name () action

599

598

600−-- | A version of liftIO that puts errors into the exception type of the Idris monad

599+-- | A version of liftIO that puts errors into the exception type of

600+-- the Idris monad

601runIO :: IO a -> Idris a

602runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

603-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"

@@ -611,8 +611,10 @@ getName = do i <- getIState;

611 putIState $ (i { idris_name = idx + 1 })

612 return idx

613

614−-- InternalApp keeps track of the real function application for making case splits from, not the application the

614+-- | InternalApp keeps track of the real function application for

615+-- making case splits from, not the application the programmer wrote,

615−-- programmer wrote, which doesn't have the whole context in any case other than top level definitions

616+-- which doesn't have the whole context in any case other than top

617+-- level definitions

616addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

618addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

617addInternalApp fp l t

619addInternalApp fp l t

618 = do i <- getIState

620 = do i <- getIState

@@ -637,16 +639,17 @@ getInternalApp fp l = do i <- getIState

637 -- TODO: What if it's not there?

639 -- TODO: What if it's not there?

638 else return Placeholder

640 else return Placeholder

639

641

640−-- Pattern definitions are only used for coverage checking, so erase them

642+-- | Pattern definitions are only used for coverage checking, so erase

641−-- when we're done

643+-- them when we're done

642clearOrigPats :: Idris ()

644clearOrigPats :: Idris ()

643clearOrigPats = do i <- get

645clearOrigPats = do i <- get

644 let ps = idris_patdefs i

646 let ps = idris_patdefs i

645 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps

647 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps

646 put (i { idris_patdefs = ps' })

648 put (i { idris_patdefs = ps' })

647

649

648−-- Erase types from Ps in the context (basically ending up with what's in

650+-- | Erase types from Ps in the context (basically ending up with

649−-- the .ibc, which is all we need after all the analysis is done)

651+-- what's in the .ibc, which is all we need after all the analysis is

652+-- done)

650clearPTypes :: Idris ()

653clearPTypes :: Idris ()

651clearPTypes = do i <- get

654clearPTypes = do i <- get

652 let ctxt = tt_ctxt i

655 let ctxt = tt_ctxt i

@@ -866,8 +869,8 @@ removeOptimise :: Optimisation -> Idris ()

866removeOptimise opt = do opts <- getOptimise

869removeOptimise opt = do opts <- getOptimise

867 setOptimise ((nub opts) \\ [opt])

870 setOptimise ((nub opts) \\ [opt])

868

871

869−-- Set appropriate optimisation set for the given level. We only have

872+-- | Set appropriate optimisation set for the given level. We only

870−-- one optimisation that is configurable at the moment, however!

873+-- have one optimisation that is configurable at the moment, however!

871setOptLevel :: Int -> Idris ()

874setOptLevel :: Int -> Idris ()

872setOptLevel n | n <= 0 = setOptimise []

875setOptLevel n | n <= 0 = setOptimise []

873setOptLevel 1 = setOptimise []

876setOptLevel 1 = setOptimise []

@@ -1350,12 +1353,11 @@ expandInstanceScope ist dec ps ns (PInstance doc argDocs info f cs pnames acc op

1350 ty cn decls

1353 ty cn decls

1351expandInstanceScope ist dec ps ns d = d

1354expandInstanceScope ist dec ps ns d = d

1352

1355

1353−-- Calculate a priority for a type, for deciding elaboration order

1356+-- | Calculate a priority for a type, for deciding elaboration order

1354-- * if it's just a type variable or concrete type, do it early (0)

1357-- * if it's just a type variable or concrete type, do it early (0)

1355-- * if there's only type variables and injective constructors, do it next (1)

1358-- * if there's only type variables and injective constructors, do it next (1)

1356-- * if there's a function type, next (2)

1359-- * if there's a function type, next (2)

1357-- * finally, everything else (3)

1360-- * finally, everything else (3)

1358−

1359getPriority :: IState -> PTerm -> Int

1361getPriority :: IState -> PTerm -> Int

1360getPriority i tm = 1 -- pri tm

1362getPriority i tm = 1 -- pri tm

1361 where

1363 where

@@ -1501,7 +1503,7 @@ addUsingConstraints syn fc t

1501 getName (PExp _ _ _ (PRef _ _ n)) = return n

1503 getName (PExp _ _ _ (PRef _ _ n)) = return n

1502 getName _ = []

1504 getName _ = []

1503

1505

1504−-- Add implicit bindings from using block, and bind any missing names

1506+-- | Add implicit bindings from using block, and bind any missing names

1505addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm

1507addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm

1506addUsingImpls syn n fc t

1508addUsingImpls syn n fc t

1507 = do ist <- getIState

1509 = do ist <- getIState

@@ -1623,8 +1625,8 @@ implicit' info syn ignore n ptm

1623 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1625 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1624 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

1626 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

1625

1627

1626−-- Even if auto_implicits is off, we need to call this so we record which

1628+-- | Even if auto_implicits is off, we need to call this so we record

1627−-- arguments are implicit

1629+-- which arguments are implicit

1628implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1630implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1629implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1631implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1630 let (declimps, ns') = execState (imps True [] tm) ([], [])

1632 let (declimps, ns') = execState (imps True [] tm) ([], [])

@@ -1729,7 +1731,7 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1729 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)) False)

1731 Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)) False)

1730 n NoFC Placeholder (pibind using ns sc)

1732 n NoFC Placeholder (pibind using ns sc)

1731

1733

1732−-- Add implicit arguments in function calls

1734+-- | Add implicit arguments in function calls

1733addImplPat :: IState -> PTerm -> PTerm

1735addImplPat :: IState -> PTerm -> PTerm

1734addImplPat = addImpl' True [] [] []

1736addImplPat = addImpl' True [] [] []

1735

1737

@@ -1739,10 +1741,10 @@ addImplBound ist ns = addImpl' False ns [] [] ist

1739addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

1741addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

1740addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

1742addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

1741

1743

1742−-- | Add the implicit arguments to applications in the term

1744+-- | Add the implicit arguments to applications in the term [Name]

1743−-- [Name] gives the names to always expend, even when under a binder of

1745+-- gives the names to always expend, even when under a binder of that

1744−-- that name (this is to expand methods with implicit arguments in dependent

1746+-- name (this is to expand methods with implicit arguments in

1745−-- type classes).

1747+-- dependent type classes).

1746addImpl :: [Name] -> IState -> PTerm -> PTerm

1748addImpl :: [Name] -> IState -> PTerm -> PTerm

1747addImpl = addImpl' False [] []

1749addImpl = addImpl' False [] []

1748

1750

@@ -2006,8 +2008,8 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

2006 | n == n' = Just (t, reverse acc ++ gs)

2008 | n == n' = Just (t, reverse acc ++ gs)

2007 find n (g : gs) acc = find n gs (g : acc)

2009 find n (g : gs) acc = find n gs (g : acc)

2008

2010

2009−-- return True if the second argument is an implicit argument which is

2011+-- | return True if the second argument is an implicit argument which

2010−-- expected in the implicits, or if it's not an implicit

2012+-- is expected in the implicits, or if it's not an implicit

2011impIn :: [PArg] -> PArg -> Bool

2013impIn :: [PArg] -> PArg -> Bool

2012impIn ps (PExp _ _ _ _) = True

2014impIn ps (PExp _ _ _ _) = True

2013impIn ps (PConstraint _ _ _ _) = True

2015impIn ps (PConstraint _ _ _ _) = True

@@ -2115,11 +2117,12 @@ mkPApp fc a f as = let rest = drop a as in

2115 appRest fc f [] = f

2117 appRest fc f [] = f

2116 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

2118 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

2117

2119

2120+

2121+

2118−-- Find 'static' argument positions

2122+-- | Find 'static' argument positions

2119-- (the declared ones, plus any names in argument position in the declared

2123-- (the declared ones, plus any names in argument position in the declared

2120-- statics)

2124-- statics)

2121-- FIXME: It's possible that this really has to happen after elaboration

2125-- FIXME: It's possible that this really has to happen after elaboration

2122−

2123findStatics :: IState -> PTerm -> (PTerm, [Bool])

2126findStatics :: IState -> PTerm -> (PTerm, [Bool])

2124findStatics ist tm = let (ns, ss) = fs tm

2127findStatics ist tm = let (ns, ss) = fs tm

2125 in runState (pos ns ss tm) []

2128 in runState (pos ns ss tm) []

@@ -2350,8 +2353,8 @@ shadow n n' t = sm 0 t where

2350 update oldn | n == oldn = n'

2353 update oldn | n == oldn = n'

2351 | otherwise = oldn

2354 | otherwise = oldn

2352

2355

2353−-- | Rename any binders which are repeated (so that we don't have to mess

2356+-- | Rename any binders which are repeated (so that we don't have to

2354−-- about with shadowing anywhere else).

2357+-- mess about with shadowing anywhere else).

2355mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2358mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2356mkUniqueNames env shadows tm

2359mkUniqueNames env shadows tm

2357 = evalState (mkUniq 0 initMap tm) (S.fromList env) where

2360 = evalState (mkUniq 0 initMap tm) (S.fromList env) where

src/Idris/AbsSyntaxTree.hs+496−412

@@ -48,23 +48,24 @@ import Text.PrettyPrint.Annotated.Leijen

48data ElabWhat = ETypes | EDefns | EAll

49 deriving (Show, Eq)

51−-- Data to pass to recursively called elaborators; e.g. for where blocks,

51+-- | Data to pass to recursively called elaborators; e.g. for where blocks,

52-- paramaterised declarations, etc.

53−

53+--

54-- rec_elabDecl is used to pass the top level elaborator into other elaborators,

55-- so that we can have mutually recursive elaborators in separate modules without

56-- having to muck about with cyclic modules.

57−data ElabInfo = EInfo { params :: [(Name, PTerm)],

57+data ElabInfo = EInfo {

58+ params :: [(Name, PTerm)]

58− inblock :: Ctxt [Name], -- names in the block, and their params

59+ , inblock :: Ctxt [Name] -- ^ names in the block, and their params

59− liftname :: Name -> Name,

60+ , liftname :: Name -> Name

60− namespace :: Maybe [String],

61+ , namespace :: Maybe [String]

61− elabFC :: Maybe FC,

62+ , elabFC :: Maybe FC

63+

62− -- We may, recursively, collect transformations to

64+ -- | We may, recursively, collect transformations to do on the rhs,

63− -- do on the rhs, e.g. rewriting recursive calls to

65+ -- e.g. rewriting recursive calls to functions defined by 'with'

64− -- functions defined by 'with'

65− rhs_trans :: PTerm -> PTerm,

66+ , rhs_trans :: PTerm -> PTerm

66− rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

67+ , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

67− Idris () }

68+ }

69toplevel :: ElabInfo

70toplevel :: ElabInfo

70toplevel = EInfo [] emptyContext id Nothing Nothing id (\_ _ _ -> fail "Not implemented")

71toplevel = EInfo [] emptyContext id Nothing Nothing id (\_ _ _ -> fail "Not implemented")

@@ -90,13 +91,13 @@ data IOption = IOption {

90 , opt_importdirs :: [FilePath]

91 , opt_importdirs :: [FilePath]

91 , opt_triple :: String

92 , opt_triple :: String

92 , opt_cpu :: String

93 , opt_cpu :: String

93− , opt_cmdline :: [Opt] -- remember whole command line

94+ , opt_cmdline :: [Opt] -- ^ remember whole command line

94 , opt_origerr :: Bool

95 , opt_origerr :: Bool

95 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover

96 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover

96− , opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude

97+ , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`

97 , opt_optimise :: [Optimisation]

98 , opt_optimise :: [Optimisation]

98 , opt_printdepth :: Maybe Int

99 , opt_printdepth :: Maybe Int

99− , opt_evaltypes :: Bool -- ^ normalise types in :t

100+ , opt_evaltypes :: Bool -- ^ normalise types in `:t`

100 , opt_desugarnats :: Bool

101 , opt_desugarnats :: Bool

101 , opt_autoimpls :: Bool

102 , opt_autoimpls :: Bool

102 } deriving (Show, Eq)

103 } deriving (Show, Eq)

@@ -130,39 +131,43 @@ defaultOpts = IOption { opt_logLevel = 0

130 }

131 }

131

132

132data PPOption = PPOption {

133data PPOption = PPOption {

133− ppopt_impl :: Bool -- ^^ whether to show implicits

134+ ppopt_impl :: Bool -- ^ whether to show implicits

134 , ppopt_desugarnats :: Bool

135 , ppopt_desugarnats :: Bool

135− , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings

136+ , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings

136− , ppopt_depth :: Maybe Int

137+ , ppopt_depth :: Maybe Int

137−} deriving (Show)

138+ } deriving (Show)

138

139

139−data Optimisation = PETransform -- partial eval and associated transforms

140+data Optimisation = PETransform -- ^ partial eval and associated transforms

140 deriving (Show, Eq)

141 deriving (Show, Eq)

141

142

142defaultOptimise = [PETransform]

143defaultOptimise = [PETransform]

143

144

144-- | Pretty printing options with default verbosity.

145-- | Pretty printing options with default verbosity.

145defaultPPOption :: PPOption

146defaultPPOption :: PPOption

146−defaultPPOption = PPOption { ppopt_impl = False,

147+defaultPPOption = PPOption {

148+ ppopt_impl = False

147− ppopt_desugarnats = False,

149+ , ppopt_desugarnats = False

148− ppopt_pinames = False,

150+ , ppopt_pinames = False

149− ppopt_depth = Just 200 }

151+ , ppopt_depth = Just 200

152+ }

150

153

151-- | Pretty printing options with the most verbosity.

154-- | Pretty printing options with the most verbosity.

152verbosePPOption :: PPOption

155verbosePPOption :: PPOption

153−verbosePPOption = PPOption { ppopt_impl = True,

156+verbosePPOption = PPOption {

157+ ppopt_impl = True

154− ppopt_desugarnats = True,

158+ , ppopt_desugarnats = True

155− ppopt_pinames = True,

159+ , ppopt_pinames = True

156− ppopt_depth = Just 200 }

160+ , ppopt_depth = Just 200

161+ }

157

162

158-- | Get pretty printing options from the big options record.

163-- | Get pretty printing options from the big options record.

159ppOption :: IOption -> PPOption

164ppOption :: IOption -> PPOption

160ppOption opt = PPOption {

165ppOption opt = PPOption {

161− ppopt_impl = opt_showimp opt,

166+ ppopt_impl = opt_showimp opt

162− ppopt_pinames = False,

167+ , ppopt_pinames = False

163− ppopt_depth = opt_printdepth opt,

168+ , ppopt_depth = opt_printdepth opt

164− ppopt_desugarnats = opt_desugarnats opt

169+ , ppopt_desugarnats = opt_desugarnats opt

165−}

170+ }

166

171

167-- | Get pretty printing options from an idris state record.

172-- | Get pretty printing options from an idris state record.

168ppOptionIst :: IState -> PPOption

173ppOptionIst :: IState -> PPOption

@@ -171,13 +176,13 @@ ppOptionIst = ppOption . idris_options

171data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

176data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

172

177

173-- | The output mode in use

178-- | The output mode in use

174−data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

179+data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

175 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle

180 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle

176 deriving Show

181 deriving Show

177

182

178-- | How wide is the console?

183-- | How wide is the console?

179data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

184data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

180− | ColsWide Int -- ^ Manually specified - must be positive

185+ | ColsWide Int -- ^ Manually specified - must be positive

181 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

186 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

182 deriving (Show, Eq)

187 deriving (Show, Eq)

183

188

@@ -189,97 +194,105 @@ data DefaultTotality = DefaultCheckingTotal -- ^ Total

189

194

190-- | The global state used in the Idris monad

195-- | The global state used in the Idris monad

191data IState = IState {

196data IState = IState {

192− tt_ctxt :: Context, -- ^ All the currently defined names and their terms

197+ tt_ctxt :: Context -- ^ All the currently defined names and their terms

193− idris_constraints :: S.Set ConstraintFC,

194− -- ^ A list of universe constraints and their corresponding source locations

198+ , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations

195− idris_infixes :: [FixDecl], -- ^ Currently defined infix operators

199+ , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators

196− idris_implicits :: Ctxt [PArg],

200+ , idris_implicits :: Ctxt [PArg]

197− idris_statics :: Ctxt [Bool],

201+ , idris_statics :: Ctxt [Bool]

198− idris_classes :: Ctxt ClassInfo,

202+ , idris_classes :: Ctxt ClassInfo

199− idris_openimpls :: [Name], -- ^ Privileged implementations, will resolve immediately

203+ , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately

200− idris_records :: Ctxt RecordInfo,

204+ , idris_records :: Ctxt RecordInfo

201− idris_dsls :: Ctxt DSL,

205+ , idris_dsls :: Ctxt DSL

202− idris_optimisation :: Ctxt OptInfo,

206+ , idris_optimisation :: Ctxt OptInfo

203− idris_datatypes :: Ctxt TypeInfo,

207+ , idris_datatypes :: Ctxt TypeInfo

204− idris_namehints :: Ctxt [Name],

208+ , idris_namehints :: Ctxt [Name]

205− idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported

209+

206− -- ^ list of lhs/rhs, and a list of missing clauses

210+ -- | list of lhs/rhs, and a list of missing clauses. These are not

211+ -- exported.

212+ , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])

207− idris_flags :: Ctxt [FnOpt],

213+ , idris_flags :: Ctxt [FnOpt]

208− idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

214+ , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos

209− idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),

215+ , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])

210− idris_moduledocs :: Ctxt (Docstring DocTerm),

216+

211− -- ^ module documentation is saved in a special MN so the context

217+ -- | module documentation is saved in a special MN so the context

212− -- mechanism can be used for disambiguation

218+ -- mechanism can be used for disambiguation.

219+ , idris_moduledocs :: Ctxt (Docstring DocTerm)

213− idris_tyinfodata :: Ctxt TIData,

220+ , idris_tyinfodata :: Ctxt TIData

214− idris_fninfo :: Ctxt FnInfo,

221+ , idris_fninfo :: Ctxt FnInfo

215− idris_transforms :: Ctxt [(Term, Term)],

222+ , idris_transforms :: Ctxt [(Term, Term)]

216− idris_autohints :: Ctxt [Name],

223+ , idris_autohints :: Ctxt [Name]

217− idris_totcheck :: [(FC, Name)], -- names to check totality on

224+ , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on

218− idris_defertotcheck :: [(FC, Name)], -- names to check at the end

225+ , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end

219− idris_totcheckfail :: [(FC, String)],

226+ , idris_totcheckfail :: [(FC, String)]

220− idris_options :: IOption,

227+ , idris_options :: IOption

221− idris_name :: Int,

228+ , idris_name :: Int

222− idris_lineapps :: [((FilePath, Int), PTerm)],

229+ , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line

223− -- ^ Full application LHS on source line

230+

224− idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))],

225− -- ^ The currently defined but not proven metavariables. The Int

231+ -- | The currently defined but not proven metavariables. The Int is

226− -- is the number of vars to display as a context, the Maybe Name

232+ -- the number of vars to display as a context, the Maybe Name is its

227− -- is its top-level function, the [Name] is the list of local variables

233+ -- top-level function, the [Name] is the list of local variables

228− -- available for proof search and the Bools are whether :p is

234+ -- available for proof search and the Bools are whether :p is

229− -- allowed, and whether the variable is definable at all

235+ -- allowed, and whether the variable is definable at all

230− -- (Metavariables are not definable if they are applied in a term which

236+ -- (Metavariables are not definable if they are applied in a term

231− -- still has hole bindings)

237+ -- which still has hole bindings)

238+ , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]

232− idris_coercions :: [Name],

239+ , idris_coercions :: [Name]

233− idris_errRev :: [(Term, Term)],

240+ , idris_errRev :: [(Term, Term)]

234− syntax_rules :: SyntaxRules,

241+ , syntax_rules :: SyntaxRules

235− syntax_keywords :: [String],

242+ , syntax_keywords :: [String]

236− imported :: [FilePath], -- ^ The imported modules

243+ , imported :: [FilePath] -- ^ The imported modules

237− idris_scprims :: [(Name, (Int, PrimFn))],

244+ , idris_scprims :: [(Name, (Int, PrimFn))]

238− idris_objs :: [(Codegen, FilePath)],

245+ , idris_objs :: [(Codegen, FilePath)]

239− idris_libs :: [(Codegen, String)],

246+ , idris_libs :: [(Codegen, String)]

240− idris_cgflags :: [(Codegen, String)],

247+ , idris_cgflags :: [(Codegen, String)]

241− idris_hdrs :: [(Codegen, String)],

248+ , idris_hdrs :: [(Codegen, String)]

242− idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public

249+ , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public

243− proof_list :: [(Name, (Bool, [String]))],

250+ , proof_list :: [(Name, (Bool, [String]))]

244− errSpan :: Maybe FC,

251+ , errSpan :: Maybe FC

245− parserWarnings :: [(FC, Err)],

252+ , parserWarnings :: [(FC, Err)]

246− lastParse :: Maybe Name,

253+ , lastParse :: Maybe Name

247− indent_stack :: [Int],

254+ , indent_stack :: [Int]

248− brace_stack :: [Maybe Int],

255+ , brace_stack :: [Maybe Int]

249− lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?

256+ , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?

250− idris_parsedSpan :: Maybe FC,

257+ , idris_parsedSpan :: Maybe FC

251− hide_list :: Ctxt Accessibility,

258+ , hide_list :: Ctxt Accessibility

252− default_access :: Accessibility,

259+ , default_access :: Accessibility

253− default_total :: DefaultTotality,

260+ , default_total :: DefaultTotality

254− ibc_write :: [IBCWrite],

261+ , ibc_write :: [IBCWrite]

255− compiled_so :: Maybe String,

262+ , compiled_so :: Maybe String

256− idris_dynamic_libs :: [DynamicLib],

263+ , idris_dynamic_libs :: [DynamicLib]

257− idris_language_extensions :: [LanguageExt],

264+ , idris_language_extensions :: [LanguageExt]

258− idris_outputmode :: OutputMode,

265+ , idris_outputmode :: OutputMode

259− idris_colourRepl :: Bool,

266+ , idris_colourRepl :: Bool

260− idris_colourTheme :: ColourTheme,

267+ , idris_colourTheme :: ColourTheme

261− idris_errorhandlers :: [Name], -- ^ Global error handlers

268+ , idris_errorhandlers :: [Name] -- ^ Global error handlers

262− idris_nameIdx :: (Int, Ctxt (Int, Name)),

269+ , idris_nameIdx :: (Int, Ctxt (Int, Name))

263− idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

270+ , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers

264− module_aliases :: M.Map [T.Text] [T.Text],

271+ , module_aliases :: M.Map [T.Text] [T.Text]

265− idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?

272+ , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?

266− idris_postulates :: S.Set Name,

273+ , idris_postulates :: S.Set Name

267− idris_externs :: S.Set (Name, Int),

274+ , idris_externs :: S.Set (Name, Int)

268− idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used

275+ , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used

269− idris_whocalls :: Maybe (M.Map Name [Name]),

276+ , idris_whocalls :: Maybe (M.Map Name [Name])

270− idris_callswho :: Maybe (M.Map Name [Name]),

277+ , idris_callswho :: Maybe (M.Map Name [Name])

278+

271− idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

279+ -- | List of names that were defined in the repl, and can be re-/un-defined

280+ , idris_repl_defs :: [Name]

281+

272− elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance

282+ -- | Stack of names currently being elaborated, Bool set if it's an

273− -- (instances appear twice; also as a funtion name)

283+ -- instance (instances appear twice; also as a funtion name)

284+ , elab_stack :: [(Name, Bool)]

285+

286+

274− idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

287+ , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

275− idris_exports :: [Name], -- ^ Functions with ExportList

288+ , idris_exports :: [Name] -- ^ Functions with ExportList

276− idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output

289+ , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output

277− idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser

290+ , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser

278− idris_deprecated :: Ctxt String, -- ^ Deprecated names and explanation

291+ , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation

279− idris_inmodule :: S.Set Name, -- ^ Names defined in current module

292+ , idris_inmodule :: S.Set Name -- ^ Names defined in current module

280− idris_ttstats :: M.Map Term (Int, Term),

293+ , idris_ttstats :: M.Map Term (Int, Term)

281− idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

294+ , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

282− }

295+ }

283

296

284-- Required for parsers library, and therefore trifecta

297-- Required for parsers library, and therefore trifecta

285instance Show IState where

298instance Show IState where

@@ -295,20 +308,21 @@ deriving instance NFData SizeChange

295type SCGEntry = (Name, [Maybe (Int, SizeChange)])

308type SCGEntry = (Name, [Maybe (Int, SizeChange)])

296type UsageReason = (Name, Int) -- fn_name, its_arg_number

309type UsageReason = (Name, Int) -- fn_name, its_arg_number

297

310

298−data CGInfo = CGInfo { calls :: [Name],

311+data CGInfo = CGInfo {

312+ calls :: [Name]

299− scg :: [SCGEntry],

313+ , scg :: [SCGEntry]

300− usedpos :: [(Int, [UsageReason])]

314+ , usedpos :: [(Int, [UsageReason])]

301− }

302− deriving Show

315+ } deriving Show

303{-!

316{-!

304deriving instance Binary CGInfo

317deriving instance Binary CGInfo

305deriving instance NFData CGInfo

318deriving instance NFData CGInfo

306!-}

319!-}

307

320

308−primDefs = [sUN "unsafePerformPrimIO",

321+primDefs = [ sUN "unsafePerformPrimIO"

309− sUN "mkLazyForeignPrim",

322+ , sUN "mkLazyForeignPrim"

310− sUN "mkForeignPrim",

323+ , sUN "mkForeignPrim"

311− sUN "void"]

324+ , sUN "void"

325+ ]

312

326

313-- information that needs writing for the current module's .ibc file

327-- information that needs writing for the current module's .ibc file

314data IBCWrite = IBCFix FixDecl

328data IBCWrite = IBCFix FixDecl

@@ -323,7 +337,7 @@ data IBCWrite = IBCFix FixDecl

323 | IBCMetavar Name

337 | IBCMetavar Name

324 | IBCSyntax Syntax

338 | IBCSyntax Syntax

325 | IBCKeyword String

339 | IBCKeyword String

326− | IBCImport (Bool, FilePath) -- True = import public

340+ | IBCImport (Bool, FilePath) -- ^ True = import public

327 | IBCImportDir FilePath

341 | IBCImportDir FilePath

328 | IBCObj Codegen FilePath

342 | IBCObj Codegen FilePath

329 | IBCLib Codegen String

343 | IBCLib Codegen String

@@ -341,7 +355,7 @@ data IBCWrite = IBCFix FixDecl

341 | IBCCG Name

355 | IBCCG Name

342 | IBCDoc Name

356 | IBCDoc Name

343 | IBCCoercion Name

357 | IBCCoercion Name

344− | IBCDef Name -- i.e. main context

358+ | IBCDef Name -- ^ The main context.

345 | IBCNameHint (Name, Name)

359 | IBCNameHint (Name, Name)

346 | IBCLineApp FilePath Int PTerm

360 | IBCLineApp FilePath Int PTerm

347 | IBCErrorHandler Name

361 | IBCErrorHandler Name

@@ -373,9 +387,13 @@ idrisInit = IState initContext S.empty []

373 emptyContext S.empty M.empty emptyContext

387 emptyContext S.empty M.empty emptyContext

374

388

375

389

376−-- | The monad for the main REPL - reading and processing files and updating

390+-- | The monad for the main REPL - reading and processing files and

377−-- global state (hence the IO inner monad).

391+-- updating global state (hence the IO inner monad).

392+--

393+-- @

378−--type Idris = WriterT [Either String (IO ())] (State IState a))

394+-- type Idris = WriterT [Either String (IO ())] (State IState a))

395+-- @

396+--

379type Idris = StateT IState (ExceptT Err IO)

397type Idris = StateT IState (ExceptT Err IO)

380

398

381catchError :: Idris a -> (Err -> Idris a) -> Idris a

399catchError :: Idris a -> (Err -> Idris a) -> Idris a

@@ -441,10 +459,10 @@ data Command = Quit

441 | MakeWith Bool Int Name

459 | MakeWith Bool Int Name

442 | MakeCase Bool Int Name

460 | MakeCase Bool Int Name

443 | MakeLemma Bool Int Name

461 | MakeLemma Bool Int Name

444− | DoProofSearch Bool -- update file

462+ | DoProofSearch Bool -- update file

445− Bool -- recursive search

463+ Bool -- recursive search

446− Int -- depth

464+ Int -- depth

447− Name -- top level name

465+ Name -- top level name

448 [Name] -- hints

466 [Name] -- hints

449 | SetOpt Opt

467 | SetOpt Opt

450 | UnsetOpt Opt

468 | UnsetOpt Opt

@@ -459,7 +477,7 @@ data Command = Quit

459 | WhoCalls Name

477 | WhoCalls Name

460 | CallsWho Name

478 | CallsWho Name

461 | Browse [String]

479 | Browse [String]

462− | MakeDoc String -- IdrisDoc

480+ | MakeDoc String -- IdrisDoc

463 | Warranty

481 | Warranty

464 | PrintDef Name

482 | PrintDef Name

465 | PPrint OutputFmt Int PTerm

483 | PPrint OutputFmt Int PTerm

@@ -538,7 +556,7 @@ data Opt = Filename String

538 | ErrContext

556 | ErrContext

539 | ShowImpl

557 | ShowImpl

540 | Verbose

558 | Verbose

541− | Port String -- REPL TCP port

559+ | Port String -- ^ REPL TCP port

542 | IBCSubDir String

560 | IBCSubDir String

543 | ImportDir String

561 | ImportDir String

544 | PkgBuild String

562 | PkgBuild String

@@ -546,7 +564,7 @@ data Opt = Filename String

546 | PkgClean String

564 | PkgClean String

547 | PkgCheck String

565 | PkgCheck String

548 | PkgREPL String

566 | PkgREPL String

549− | PkgMkDoc String -- IdrisDoc

567+ | PkgMkDoc String -- IdrisDoc

550 | PkgTest String

568 | PkgTest String

551 | PkgIndex FilePath

569 | PkgIndex FilePath

552 | WarnOnly

570 | WarnOnly

@@ -572,20 +590,26 @@ data Opt = Filename String

572 | UseConsoleWidth ConsoleWidth

590 | UseConsoleWidth ConsoleWidth

573 | DumpHighlights

591 | DumpHighlights

574 | DesugarNats

592 | DesugarNats

575− | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

593+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

576 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

594 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

577 deriving (Show, Eq)

595 deriving (Show, Eq)

578

596

579−data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

597+data ElabShellCmd = EQED

598+ | EAbandon

599+ | EUndo

600+ | EProofState

601+ | EProofTerm

602+ | EEval PTerm

603+ | ECheck PTerm

580− | EEval PTerm | ECheck PTerm | ESearch PTerm

604+ | ESearch PTerm

581 | EDocStr (Either Name Const)

605 | EDocStr (Either Name Const)

582 deriving (Show, Eq)

606 deriving (Show, Eq)

583

607

584-- Parsed declarations

608-- Parsed declarations

585

609

586−data Fixity = Infixl { prec :: Int }

610+data Fixity = Infixl { prec :: Int }

587− | Infixr { prec :: Int }

611+ | Infixr { prec :: Int }

588− | InfixN { prec :: Int }

612+ | InfixN { prec :: Int }

589 | PrefixN { prec :: Int }

613 | PrefixN { prec :: Int }

590 deriving Eq

614 deriving Eq

591{-!

615{-!

@@ -594,9 +618,9 @@ deriving instance NFData Fixity

594!-}

618!-}

595

619

596instance Show Fixity where

620instance Show Fixity where

597− show (Infixl i) = "infixl " ++ show i

621+ show (Infixl i) = "infixl " ++ show i

598− show (Infixr i) = "infixr " ++ show i

622+ show (Infixr i) = "infixr " ++ show i

599− show (InfixN i) = "infix " ++ show i

623+ show (InfixN i) = "infix " ++ show i

600 show (PrefixN i) = "prefix " ++ show i

624 show (PrefixN i) = "prefix " ++ show i

601

625

602data FixDecl = Fix Fixity String

626data FixDecl = Fix Fixity String

@@ -621,22 +645,25 @@ deriving instance Binary Static

621deriving instance NFData Static

645deriving instance NFData Static

622!-}

646!-}

623

647

624−-- Mark bindings with their explicitness, and laziness

648+-- ^ Mark bindings with their explicitness, and laziness

625−data Plicity = Imp { pargopts :: [ArgOpt],

649+data Plicity = Imp { pargopts :: [ArgOpt]

626− pstatic :: Static,

650+ , pstatic :: Static

627− pparam :: Bool,

651+ , pparam :: Bool

628− pscoped :: Maybe ImplicitInfo, -- Nothing, if top level

652+ , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level

629− pinsource :: Bool -- Explicitly written in source

653+ , pinsource :: Bool -- ^ Explicitly written in source

630 }

654 }

631− | Exp { pargopts :: [ArgOpt],

655+ | Exp { pargopts :: [ArgOpt]

632− pstatic :: Static,

656+ , pstatic :: Static

633− pparam :: Bool } -- this is a param (rather than index)

657+ , pparam :: Bool -- ^ this is a param (rather than index)

658+ }

634− | Constraint { pargopts :: [ArgOpt],

659+ | Constraint { pargopts :: [ArgOpt]

635− pstatic :: Static }

660+ , pstatic :: Static

661+ }

636− | TacImp { pargopts :: [ArgOpt],

662+ | TacImp { pargopts :: [ArgOpt]

637− pstatic :: Static,

663+ , pstatic :: Static

638− pscript :: PTerm }

664+ , pscript :: PTerm

665+ }

639− deriving (Show, Eq, Data, Typeable)

666+ deriving (Show, Eq, Data, Typeable)

640

667

641{-!

668{-!

642deriving instance Binary Plicity

669deriving instance Binary Plicity

@@ -645,7 +672,7 @@ deriving instance NFData Plicity

645

672

646is_scoped :: Plicity -> Maybe ImplicitInfo

673is_scoped :: Plicity -> Maybe ImplicitInfo

647is_scoped (Imp _ _ _ s _) = s

674is_scoped (Imp _ _ _ s _) = s

648−is_scoped _ = Nothing

675+is_scoped _ = Nothing

649

676

650impl = Imp [] Dynamic False (Just (Impl False True)) False

677impl = Imp [] Dynamic False (Just (Impl False True)) False

651

678

@@ -659,21 +686,23 @@ constraint = Constraint [] Static

659

686

660tacimpl t = TacImp [] Dynamic t

687tacimpl t = TacImp [] Dynamic t

661

688

662−data FnOpt = Inlinable -- always evaluate when simplifying

689+data FnOpt = Inlinable -- ^ always evaluate when simplifying

663 | TotalFn | PartialFn | CoveringFn

690 | TotalFn | PartialFn | CoveringFn

664 | Coinductive | AssertTotal

691 | Coinductive | AssertTotal

692+

665− | Dictionary -- type class dictionary, eval only when

693+ -- | type class dictionary, eval only when a function

666− -- a function argument, and further evaluation resutls

694+ -- argument, and further evaluation results.

695+ | Dictionary

667− | Implicit -- implicit coercion

696+ | Implicit -- ^ implicit coercion

668− | NoImplicit -- do not apply implicit coercions

697+ | NoImplicit -- ^ do not apply implicit coercions

669− | CExport String -- export, with a C name

698+ | CExport String -- ^ export, with a C name

670− | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

699+ | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension

671− | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

700+ | ErrorReverse -- ^ attempt to reverse normalise before showing in error

672− | Reflection -- a reflecting function, compile-time only

701+ | Reflection -- ^ a reflecting function, compile-time only

673− | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

702+ | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names

674− | Constructor -- Data constructor type

703+ | Constructor -- ^ Data constructor type

675− | AutoHint -- use in auto implicit search

704+ | AutoHint -- ^ use in auto implicit search

676− | PEGenerated -- generated by partial evaluator

705+ | PEGenerated -- ^ generated by partial evaluator

677 deriving (Show, Eq)

706 deriving (Show, Eq)

678{-!

707{-!

679deriving instance Binary FnOpt

708deriving instance Binary FnOpt

@@ -699,67 +728,84 @@ type ProvideWhat = ProvideWhat' PTerm

699-- | Top-level declarations such as compiler directives, definitions,

728-- | Top-level declarations such as compiler directives, definitions,

700-- datatypes and typeclasses.

729-- datatypes and typeclasses.

701data PDecl' t

730data PDecl' t

731+ -- | Fixity declaration

702− = PFix FC Fixity [String] -- ^ Fixity declaration

732+ = PFix FC Fixity [String]

733+ -- | Type declaration (last FC is precise name location)

703− | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)

734+ | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t

735+ -- | Postulate, second FC is precise name location

704 | PPostulate Bool -- external def if true

736 | PPostulate Bool -- external def if true

705− (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location

737+ (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t

738+ -- | Pattern clause

706− | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

739+ | PClauses FC FnOpts Name [PClause' t]

707− | PCAF FC Name t -- ^ Top level constant

740+ -- | Top level constant

708− | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

741+ | PCAF FC Name t

742+ -- | Data declaration.

743+ | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)

709− | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

744+ -- | Params block

745+ | PParams FC [(Name, t)] [PDecl' t]

710− | POpenInterfaces FC [Name] [PDecl' t] -- ^ Open block/declaration

746+ -- | Open block/declaration

747+ | POpenInterfaces FC [Name] [PDecl' t]

748+ -- | New namespace, where FC is accurate location of the namespace

749+ -- in the file

711 | PNamespace String FC [PDecl' t]

750 | PNamespace String FC [PDecl' t]

712− -- ^ New namespace, where FC is accurate location of the

751+ -- | Record name.

713− -- namespace in the file

714− | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts

752+ | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts

715− Name -- Record name

753+ Name -- Record name

716− FC -- Record name precise location

754+ FC -- Record name precise location

717− [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

755+ [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

718− [(Name, Docstring (Either Err t))] -- Param Docs

756+ [(Name, Docstring (Either Err t))] -- Param Docs

719− [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields

757+ [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields

720− (Maybe (Name, FC)) -- Optional constructor name and location

758+ (Maybe (Name, FC)) -- Optional constructor name and location

721− (Docstring (Either Err t)) -- Constructor doc

759+ (Docstring (Either Err t)) -- Constructor doc

722− SyntaxInfo -- Constructor SyntaxInfo

760+ SyntaxInfo -- Constructor SyntaxInfo

723− -- ^ Record declaration

761+

762+ -- | Type class: arguments are documentation, syntax info, source

763+ -- location, constraints, class name, class name location,

764+ -- parameters, method declarations, optional constructor name

724− | PClass (Docstring (Either Err t)) SyntaxInfo FC

765+ | PClass (Docstring (Either Err t)) SyntaxInfo FC

725− [(Name, t)] -- constraints

766+ [(Name, t)] -- constraints

726− Name -- class name

767+ Name -- class name

727− FC -- accurate location of class name

768+ FC -- accurate location of class name

728− [(Name, FC, t)] -- parameters and precise locations

769+ [(Name, FC, t)] -- parameters and precise locations

729− [(Name, Docstring (Either Err t))] -- parameter docstrings

770+ [(Name, Docstring (Either Err t))] -- parameter docstrings

730− [(Name, FC)] -- determining parameters and precise locations

771+ [(Name, FC)] -- determining parameters and precise locations

731− [PDecl' t] -- declarations

772+ [PDecl' t] -- declarations

732− (Maybe (Name, FC)) -- instance constructor name and location

773+ (Maybe (Name, FC)) -- instance constructor name and location

733− (Docstring (Either Err t)) -- instance constructor docs

774+ (Docstring (Either Err t)) -- instance constructor docs

775+

734− -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

776+ -- | Instance declaration: arguments are documentation, syntax

735− -- class name, class name location, parameters, method declarations, optional constructor name

777+ -- info, source location, constraints, class name, parameters, full

736− | PInstance

778+ -- instance type, optional explicit name, and definitions

737− (Docstring (Either Err t)) -- Instance docs

779+ | PInstance (Docstring (Either Err t)) -- Instance docs

738− [(Name, Docstring (Either Err t))] -- Parameter docs

780+ [(Name, Docstring (Either Err t))] -- Parameter docs

739− SyntaxInfo

781+ SyntaxInfo

740− FC [(Name, t)] -- constraints

782+ FC [(Name, t)] -- constraints

741− [Name] -- parent dictionaries to search for constraints

783+ [Name] -- parent dictionaries to search for constraints

742− Accessibility

784+ Accessibility

743− FnOpts

785+ FnOpts

744− Name -- class

786+ Name -- class

745− FC -- precise location of class

787+ FC -- precise location of class

746− [t] -- parameters

788+ [t] -- parameters

747− [(Name, t)] -- Extra names in scope in the body

789+ [(Name, t)] -- Extra names in scope in the body

748− t -- full instance type

790+ t -- full instance type

749− (Maybe Name) -- explicit name

791+ (Maybe Name) -- explicit name

750− [PDecl' t]

792+ [PDecl' t]

751− -- ^ Instance declaration: arguments are documentation, syntax info, source

752− -- location, constraints, class name, parameters, full instance

753− -- type, optional explicit name, and definitions

754 | PDSL Name (DSL' t) -- ^ DSL declaration

793 | PDSL Name (DSL' t) -- ^ DSL declaration

755− | PSyntax FC Syntax -- ^ Syntax definition

794+ | PSyntax FC Syntax -- ^ Syntax definition

756 | PMutual FC [PDecl' t] -- ^ Mutual block

795 | PMutual FC [PDecl' t] -- ^ Mutual block

757− | PDirective Directive -- ^ Compiler directive.

796+ | PDirective Directive -- ^ Compiler directive.

797+

758− | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.

798+ -- | Type provider. The first t is the type, the second is the

799+ -- term. The second FC is precise highlighting location.

800+ | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name

801+

759− | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

802+ -- | Source-to-source transformation rule. If bool is True, lhs and

760− -- bool is True, lhs and rhs must be convertible

803+ -- rhs must be convertible.

804+ | PTransform FC Bool t t

805+

761− | PRunElabDecl FC t [String] -- ^ FC is decl-level, for errors, and

806+ -- | FC is decl-level, for errors, and Strings represent the

762− -- Strings represent the namespace

807+ -- namespace

808+ | PRunElabDecl FC t [String]

763 deriving Functor

809 deriving Functor

764{-!

810{-!

765deriving instance Binary PDecl'

811deriving instance Binary PDecl'

@@ -792,18 +838,19 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

792 | RClausesInstrs Name [([(Name, Term)], Term, Term)]

838 | RClausesInstrs Name [([(Name, Term)], Term, Term)]

793 | RAddInstance Name Name

839 | RAddInstance Name Name

794 | RDatatypeDeclInstrs Name [PArg]

840 | RDatatypeDeclInstrs Name [PArg]

841+ -- | Datatype, constructors

795 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]

842 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]

796− -- ^ Datatype, constructors

843+

797

844

798-- | For elaborator state

845-- | For elaborator state

799data EState = EState {

846data EState = EState {

800− case_decls :: [(Name, PDecl)],

847+ case_decls :: [(Name, PDecl)]

801− delayed_elab :: [(Int, Elab' EState ())],

848+ , delayed_elab :: [(Int, Elab' EState ())]

802− new_tyDecls :: [RDeclInstructions],

849+ , new_tyDecls :: [RDeclInstructions]

803− highlighting :: [(FC, OutputAnnotation)],

850+ , highlighting :: [(FC, OutputAnnotation)]

804− auto_binds :: [Name], -- names bound as auto implicits

851+ , auto_binds :: [Name] -- ^ names bound as auto implicits

805− implicit_warnings :: [(FC, Name)] -- Implicit warnings to report (location and global name)

852+ , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)

806− }

853+ }

807

854

808initEState :: EState

855initEState :: EState

809initEState = EState [] [] [] [] [] []

856initEState = EState [] [] [] [] [] []

@@ -835,20 +882,23 @@ deriving instance NFData PClause'

835!-}

882!-}

836

883

837-- | Data declaration

884-- | Data declaration

885+data PData' t =

886+ -- | Data declaration

838−data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

887+ PDatadecl { d_name :: Name -- ^ The name of the datatype

839− d_name_fc :: FC, -- ^ The precise location of the type constructor name

888+ , d_name_fc :: FC -- ^ The precise location of the type constructor name

840− d_tcon :: t, -- ^ Type constructor

889+ , d_tcon :: t -- ^ Type constructor

841− d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors

890+ , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors

842− }

891+ }

843− -- ^ Data declaration

844− | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }

845− -- ^ "Placeholder" for data whose constructors are defined later

892+ -- | "Placeholder" for data whose constructors are defined later

893+ | PLaterdecl { d_name :: Name

894+ , d_name_fc :: FC

895+ , d_tcon :: t

846− deriving Functor

896+ } deriving Functor

847

897

848-- | Transform the FCs in a PData and its associated terms. The first

898-- | Transform the FCs in a PData and its associated terms. The first

849−-- function transforms the general-purpose FCs, and the second transforms

899+-- function transforms the general-purpose FCs, and the second

850−-- those that are used for semantic source highlighting, so they can be

900+-- transforms those that are used for semantic source highlighting, so

851−-- treated specially.

901+-- they can be treated specially.

852mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData

902mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData

853mapPDataFC f g (PDatadecl n nfc tycon ctors) =

903mapPDataFC f g (PDatadecl n nfc tycon ctors) =

854 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)

904 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)

@@ -1030,56 +1080,76 @@ updateNs ns t = mapPT updateRef t

1030-- (map (updateDNs ns) ds)

1080-- (map (updateDNs ns) ds)

1031-- updateDNs ns c = c

1081-- updateDNs ns c = c

1032

1082

1083+data PunInfo = IsType

1084+ | IsTerm

1085+ | TypeOrTerm

1033−data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)

1086+ deriving (Eq, Show, Data, Typeable)

1034

1087

1035-- | High level language terms

1088-- | High level language terms

1036−data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language

1089+data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

1090+ -- high-level language

1091+ | PRef FC [FC] Name

1092+ -- ^ A reference to a variable. The FC is its precise

1037− | PRef FC [FC] Name -- ^ A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.

1093+ -- source location for highlighting. The list of FCs is a

1094+ -- collection of additional highlighting locations.

1038− | PInferRef FC [FC] Name -- ^ A name to be defined later

1095+ | PInferRef FC [FC] Name -- ^ A name to be defined later

1039− | PPatvar FC Name -- ^ A pattern variable

1096+ | PPatvar FC Name -- ^ A pattern variable

1040− | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.

1097+ | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.

1041− | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable

1098+ | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable

1042− | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

1099+ | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

1043− | PTyped PTerm PTerm -- ^ Term with explicit type

1100+ | PTyped PTerm PTerm -- ^ Term with explicit type

1044− | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

1101+ | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

1045− | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument

1102+ | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument

1046− | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

1103+ | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

1047− | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

1104+ | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

1048− | PMatchApp FC Name -- ^ Make an application by type matching

1105+ | PMatchApp FC Name -- ^ Make an application by type matching

1049− | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse

1106+ | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse

1050− | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

1107+ | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

1051− | PTrue FC PunInfo -- ^ Unit type..?

1108+ | PTrue FC PunInfo -- ^ Unit type..?

1052− | PResolveTC FC -- ^ Solve this dictionary by type class resolution

1109+ | PResolveTC FC -- ^ Solve this dictionary by type class resolution

1053 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

1110 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

1054− -- ^ "rewrite" syntax, with optional rewriting function

1111+ -- ^ "rewrite" syntax, with optional rewriting function and

1055− -- and optional result type

1112+ -- optional result type

1113+ | PPair FC [FC] PunInfo PTerm PTerm

1114+ -- ^ A pair (a, b) and whether it's a product type or a

1056− | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

1115+ -- pair (solved by elaboration). The list of FCs is its

1116+ -- punctuation.

1117+ | PDPair FC [FC] PunInfo PTerm PTerm PTerm

1118+ -- ^ A dependent pair (tm : a ** b) and whether it's a

1057− | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.

1119+ -- sigma type or a pair that inhabits one (solved by

1120+ -- elaboration). The [FC] is its punctuation.

1058− | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

1121+ | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

1059 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

1122 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

1060− | PHidden PTerm -- ^ Irrelevant or hidden pattern

1123+ | PHidden PTerm -- ^ Irrelevant or hidden pattern

1061− | PType FC -- ^ 'Type' type

1124+ | PType FC -- ^ 'Type' type

1062− | PUniverse Universe -- ^ Some universe

1125+ | PUniverse Universe -- ^ Some universe

1063− | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

1126+ | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

1064− | PConstant FC Const -- ^ Builtin types

1127+ | PConstant FC Const -- ^ Builtin types

1065− | Placeholder -- ^ Underscore

1128+ | Placeholder -- ^ Underscore

1066− | PDoBlock [PDo] -- ^ Do notation

1129+ | PDoBlock [PDo] -- ^ Do notation

1067− | PIdiom FC PTerm -- ^ Idiom brackets

1130+ | PIdiom FC PTerm -- ^ Idiom brackets

1068 | PReturn FC

1131 | PReturn FC

1069− | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location

1132+ | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location

1070− | PProof [PTactic] -- ^ Proof script

1133+ | PProof [PTactic] -- ^ Proof script

1071− | PTactics [PTactic] -- ^ As PProof, but no auto solving

1134+ | PTactics [PTactic] -- ^ As PProof, but no auto solving

1072− | PElabError Err -- ^ Error to report on elaboration

1135+ | PElabError Err -- ^ Error to report on elaboration

1073− | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

1136+ | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

1074− | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

1137+ | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

1075− | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces

1138+ | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces

1076− | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

1139+ | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

1077− | PNoImplicits PTerm -- ^ never run implicit converions on the term

1140+ | PNoImplicits PTerm -- ^ never run implicit converions on the term

1078− | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

1141+ | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

1079− | PUnquote PTerm -- ^ ~Term

1142+ | PUnquote PTerm -- ^ ~Term

1143+ | PQuoteName Name Bool FC

1144+ -- ^ `{n} where the FC is the precise highlighting for

1080− | PQuoteName Name Bool FC -- ^ `{n} where the FC is the precise highlighting for the name in particular. If the Bool is False, then it's `{{n}} and the name won't be resolved.

1145+ -- the name in particular. If the Bool is False, then

1146+ -- it's `{{n}} and the name won't be resolved.

1147+ | PRunElab FC PTerm [String]

1081− | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.

1148+ -- ^ %runElab tm - New-style proof script. Args are

1149+ -- location, script, enclosing namespace.

1150+ | PConstSugar FC PTerm

1151+ -- ^ A desugared constant. The FC is a precise source

1082− | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.

1152+ -- location that will be used to highlight it later.

1083 deriving (Eq, Data, Typeable)

1153 deriving (Eq, Data, Typeable)

1084

1154

1085data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

1155data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

@@ -1249,9 +1319,9 @@ instance Sized a => Sized (PTactic' a) where

1249type PTactic = PTactic' PTerm

1319type PTactic = PTactic' PTerm

1250

1320

1251data PDo' t = DoExp FC t

1321data PDo' t = DoExp FC t

1252− | DoBind FC Name FC t -- ^ second FC is precise name location

1322+ | DoBind FC Name FC t -- ^ second FC is precise name location

1253 | DoBindP FC t t [(t,t)]

1323 | DoBindP FC t t [(t,t)]

1254− | DoLet FC Name FC t t -- ^ second FC is precise name location

1324+ | DoLet FC Name FC t t -- ^ second FC is precise name location

1255 | DoLetP FC t t

1325 | DoLetP FC t t

1256 deriving (Eq, Functor, Data, Typeable)

1326 deriving (Eq, Functor, Data, Typeable)

1257{-!

1327{-!

@@ -1262,9 +1332,9 @@ deriving instance NFData PDo'

1262instance Sized a => Sized (PDo' a) where

1332instance Sized a => Sized (PDo' a) where

1263 size (DoExp fc t) = 1 + size fc + size t

1333 size (DoExp fc t) = 1 + size fc + size t

1264 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t

1334 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t

1265− size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

1335+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

1266− size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r

1336+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r

1267− size (DoLetP fc l r) = 1 + size fc + size l + size r

1337+ size (DoLetP fc l r) = 1 + size fc + size l + size r

1268

1338

1269type PDo = PDo' PTerm

1339type PDo = PDo' PTerm

1270

1340

@@ -1272,33 +1342,40 @@ type PDo = PDo' PTerm

1272-- things early which will help give a more concrete type to other

1342-- things early which will help give a more concrete type to other

1273-- variables, e.g. a before (interpTy a).

1343-- variables, e.g. a before (interpTy a).

1274

1344

1275−data PArg' t = PImp { priority :: Int,

1345+data PArg' t = PImp { priority :: Int

1276− machine_inf :: Bool, -- true if the machine inferred it

1346+ , machine_inf :: Bool -- ^ true if the machine inferred it

1277− argopts :: [ArgOpt],

1347+ , argopts :: [ArgOpt]

1278− pname :: Name,

1348+ , pname :: Name

1279− getTm :: t }

1349+ , getTm :: t

1350+ }

1280− | PExp { priority :: Int,

1351+ | PExp { priority :: Int

1281− argopts :: [ArgOpt],

1352+ , argopts :: [ArgOpt]

1282− pname :: Name,

1353+ , pname :: Name

1283− getTm :: t }

1354+ , getTm :: t

1355+ }

1284− | PConstraint { priority :: Int,

1356+ | PConstraint { priority :: Int

1285− argopts :: [ArgOpt],

1357+ , argopts :: [ArgOpt]

1286− pname :: Name,

1358+ , pname :: Name

1287− getTm :: t }

1359+ , getTm :: t

1360+ }

1288− | PTacImplicit { priority :: Int,

1361+ | PTacImplicit { priority :: Int

1289− argopts :: [ArgOpt],

1362+ , argopts :: [ArgOpt]

1290− pname :: Name,

1363+ , pname :: Name

1291− getScript :: t,

1364+ , getScript :: t

1292− getTm :: t }

1365+ , getTm :: t

1366+ }

1293− deriving (Show, Eq, Functor, Data, Typeable)

1367+ deriving (Show, Eq, Functor, Data, Typeable)

1294−

1368+

1295−data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp

1369+data ArgOpt = AlwaysShow

1370+ | HideDisplay

1371+ | InaccessibleArg

1372+ | UnknownImp

1296− deriving (Show, Eq, Data, Typeable)

1373+ deriving (Show, Eq, Data, Typeable)

1297

1374

1298instance Sized a => Sized (PArg' a) where

1375instance Sized a => Sized (PArg' a) where

1299 size (PImp p _ l nm trm) = 1 + size nm + size trm

1376 size (PImp p _ l nm trm) = 1 + size nm + size trm

1300 size (PExp p l nm trm) = 1 + size nm + size trm

1377 size (PExp p l nm trm) = 1 + size nm + size trm

1301− size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm

1378+ size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm

1302 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

1379 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

1303

1380

1304{-!

1381{-!

@@ -1375,28 +1452,30 @@ highestFC (PAppImpl t _) = highestFC t

1375

1452

1376-- Type class data

1453-- Type class data

1377

1454

1455+data ClassInfo = CI {

1378−data ClassInfo = CI { instanceCtorName :: Name,

1456+ instanceCtorName :: Name

1379− class_methods :: [(Name, (Bool, FnOpts, PTerm))], -- flag whether it's a "data" method

1457+ , class_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method

1380− class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

1458+ , class_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl

1381− class_default_superclasses :: [PDecl],

1459+ , class_default_superclasses :: [PDecl]

1382− class_params :: [Name],

1460+ , class_params :: [Name]

1383− class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded

1461+ , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded

1384− class_determiners :: [Int] }

1462+ , class_determiners :: [Int]

1385− deriving Show

1463+ } deriving Show

1386{-!

1464{-!

1387deriving instance Binary ClassInfo

1465deriving instance Binary ClassInfo

1388deriving instance NFData ClassInfo

1466deriving instance NFData ClassInfo

1389!-}

1467!-}

1390

1468

1391-- Record data

1469-- Record data

1470+data RecordInfo = RI {

1392−data RecordInfo = RI { record_parameters :: [(Name,PTerm)],

1471+ record_parameters :: [(Name,PTerm)]

1393− record_constructor :: Name,

1472+ , record_constructor :: Name

1394− record_projections :: [Name] }

1473+ , record_projections :: [Name]

1395− deriving Show

1474+ } deriving Show

1396

1475

1397-- Type inference data

1476-- Type inference data

1398

1477

1399−data TIData = TIPartial -- ^ a function with a partially defined type

1478+data TIData = TIPartial -- ^ a function with a partially defined type

1400 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

1479 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

1401 deriving Show

1480 deriving Show

1402

1481

@@ -1408,27 +1487,28 @@ deriving instance Binary FnInfo

1408deriving instance NFData FnInfo

1487deriving instance NFData FnInfo

1409!-}

1488!-}

1410

1489

1490+data OptInfo = Optimise {

1411−data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting

1491+ inaccessible :: [(Int,Name)] -- includes names for error reporting

1412− detaggable :: Bool }

1492+ , detaggable :: Bool

1413− deriving Show

1493+ } deriving Show

1414{-!

1494{-!

1415deriving instance Binary OptInfo

1495deriving instance Binary OptInfo

1416deriving instance NFData OptInfo

1496deriving instance NFData OptInfo

1417!-}

1497!-}

1418

1498

1419-- | Syntactic sugar info

1499-- | Syntactic sugar info

1420−data DSL' t = DSL { dsl_bind :: t,

1500+data DSL' t = DSL {

1501+ dsl_bind :: t

1421− dsl_return :: t,

1502+ , dsl_return :: t

1422− dsl_apply :: t,

1503+ , dsl_apply :: t

1423− dsl_pure :: t,

1504+ , dsl_pure :: t

1424− dsl_var :: Maybe t,

1505+ , dsl_var :: Maybe t

1425− index_first :: Maybe t,

1506+ , index_first :: Maybe t

1426− index_next :: Maybe t,

1507+ , index_next :: Maybe t

1427− dsl_lambda :: Maybe t,

1508+ , dsl_lambda :: Maybe t

1428− dsl_let :: Maybe t,

1509+ , dsl_let :: Maybe t

1429− dsl_pi :: Maybe t

1510+ , dsl_pi :: Maybe t

1430− }

1431− deriving (Show, Functor)

1511+ } deriving (Show, Functor)

1432{-!

1512{-!

1433deriving instance Binary DSL'

1513deriving instance Binary DSL'

1434deriving instance NFData DSL'

1514deriving instance NFData DSL'

@@ -1436,7 +1516,9 @@ deriving instance NFData DSL'

1436

1516

1437type DSL = DSL' PTerm

1517type DSL = DSL' PTerm

1438

1518

1439−data SynContext = PatternSyntax | TermSyntax | AnySyntax

1519+data SynContext = PatternSyntax

1520+ | TermSyntax

1521+ | AnySyntax

1440 deriving Show

1522 deriving Show

1441{-!

1523{-!

1442deriving instance Binary SynContext

1524deriving instance Binary SynContext

@@ -1536,24 +1618,25 @@ deriving instance Binary Using

1536deriving instance NFData Using

1618deriving instance NFData Using

1537!-}

1619!-}

1538

1620

1539−data SyntaxInfo = Syn { using :: [Using],

1621+data SyntaxInfo = Syn {

1622+ using :: [Using]

1540− syn_params :: [(Name, PTerm)],

1623+ , syn_params :: [(Name, PTerm)]

1541− syn_namespace :: [String],

1624+ , syn_namespace :: [String]

1542− no_imp :: [Name],

1625+ , no_imp :: [Name]

1626+ , imp_methods :: [Name]

1543− imp_methods :: [Name], -- class methods. When expanding

1627+ -- ^ class methods. When expanding implicits, these should be

1544− -- implicits, these should be expanded even under

1628+ -- expanded even under binders

1545− -- binders

1546− decoration :: Name -> Name,

1629+ , decoration :: Name -> Name

1547− inPattern :: Bool,

1630+ , inPattern :: Bool

1548− implicitAllowed :: Bool,

1631+ , implicitAllowed :: Bool

1549− constraintAllowed :: Bool,

1632+ , constraintAllowed :: Bool

1550− maxline :: Maybe Int,

1633+ , maxline :: Maybe Int

1551− mut_nesting :: Int,

1634+ , mut_nesting :: Int

1552− dsl_info :: DSL,

1635+ , dsl_info :: DSL

1553− syn_in_quasiquote :: Int,

1636+ , syn_in_quasiquote :: Int

1554− syn_toplevel :: Bool,

1637+ , syn_toplevel :: Bool

1555− withAppAllowed :: Bool }

1638+ , withAppAllowed :: Bool

1556− deriving Show

1639+ } deriving Show

1557{-!

1640{-!

1558deriving instance NFData SyntaxInfo

1641deriving instance NFData SyntaxInfo

1559deriving instance Binary SyntaxInfo

1642deriving instance Binary SyntaxInfo

@@ -1693,9 +1776,9 @@ instance Show PData where

1693instance Pretty PTerm OutputAnnotation where

1776instance Pretty PTerm OutputAnnotation where

1694 pretty = prettyImp defaultPPOption

1777 pretty = prettyImp defaultPPOption

1695

1778

1696−-- | Colourise annotations according to an Idris state. It ignores the names

1779+-- | Colourise annotations according to an Idris state. It ignores the

1697−-- in the annotation, as there's no good way to show extended information on a

1780+-- names in the annotation, as there's no good way to show extended

1698−-- terminal.

1781+-- information on a terminal.

1699annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour

1782annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour

1700annotationColour ist _ | not (idris_colourRepl ist) = Nothing

1783annotationColour ist _ | not (idris_colourRepl ist) = Nothing

1701annotationColour ist (AnnConst c) =

1784annotationColour ist (AnnConst c) =

@@ -1724,8 +1807,8 @@ annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)

1724annotationColour ist _ = Nothing

1807annotationColour ist _ = Nothing

1725

1808

1726

1809

1727−-- | Colourise annotations according to an Idris state. It ignores the names

1810+-- | Colourise annotations according to an Idris state. It ignores the

1728−-- in the annotation, as there's no good way to show extended

1811+-- names in the annotation, as there's no good way to show extended

1729-- information on a terminal. Note that strings produced this way will

1812-- information on a terminal. Note that strings produced this way will

1730-- not be coloured on Windows, so the use of the colour rendering

1813-- not be coloured on Windows, so the use of the colour rendering

1731-- functions in Idris.Output is to be preferred.

1814-- functions in Idris.Output is to be preferred.

@@ -1735,9 +1818,10 @@ consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)

1735isPostulateName :: Name -> IState -> Bool

1818isPostulateName :: Name -> IState -> Bool

1736isPostulateName n ist = S.member n (idris_postulates ist)

1819isPostulateName n ist = S.member n (idris_postulates ist)

1737

1820

1738−-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1821+-- | Pretty-print a high-level closed Idris term with no information

1822+-- about precedence/associativity

1739−prettyImp :: PPOption -- ^^ pretty printing options

1823+prettyImp :: PPOption -- ^ pretty printing options

1740− -> PTerm -- ^^ the term to pretty-print

1824+ -> PTerm -- ^ the term to pretty-print

1741 -> Doc OutputAnnotation

1825 -> Doc OutputAnnotation

1742prettyImp impl = pprintPTerm impl [] [] []

1826prettyImp impl = pprintPTerm impl [] [] []

1743

1827

@@ -1747,12 +1831,13 @@ prettyImp impl = pprintPTerm impl [] [] []

1747prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1831prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1748prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1832prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1749

1833

1750−-- | Pretty-print a high-level Idris term in some bindings context with infix info

1834+-- | Pretty-print a high-level Idris term in some bindings context

1835+-- with infix info.

1751−pprintPTerm :: PPOption -- ^^ pretty printing options

1836+pprintPTerm :: PPOption -- ^ pretty printing options

1752− -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1837+ -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit

1753− -> [Name] -- ^^ names to always show in pi, even if not used

1838+ -> [Name] -- ^ names to always show in pi, even if not used

1754− -> [FixDecl] -- ^^ Fixity declarations

1839+ -> [FixDecl] -- ^ Fixity declarations

1755− -> PTerm -- ^^ the term to pretty-print

1840+ -> PTerm -- ^ the term to pretty-print

1756 -> Doc OutputAnnotation

1841 -> Doc OutputAnnotation

1757pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1842pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1758 where

1843 where

@@ -2125,8 +2210,8 @@ basename :: Name -> Name

2125basename (NS n _) = basename n

2210basename (NS n _) = basename n

2126basename n = n

2211basename n = n

2127

2212

2128−-- | Determine whether a name was the one inserted for a hole or

2213+-- | Determine whether a name was the one inserted for a hole or guess

2129−-- guess by the delaborator

2214+-- by the delaborator

2130isHoleName :: Name -> Bool

2215isHoleName :: Name -> Bool

2131isHoleName (UN n) = n == T.pack "[__]"

2216isHoleName (UN n) = n == T.pack "[__]"

2132isHoleName _ = False

2217isHoleName _ = False

@@ -2136,12 +2221,11 @@ containsHole :: PTerm -> Bool

2136containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]

2221containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]

2137

2222

2138-- | Pretty-printer helper for names that attaches the correct annotations

2223-- | Pretty-printer helper for names that attaches the correct annotations

2139−prettyName

2140− :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator

2224+prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator

2141− -> Bool -- ^^ whether to show namespaces

2225+ -> Bool -- ^ whether to show namespaces

2142− -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit

2226+ -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit

2143− -> Name -- ^^ the name to pprint

2227+ -> Name -- ^ the name to pprint

2144− -> Doc OutputAnnotation

2228+ -> Doc OutputAnnotation

2145prettyName infixParen showNS bnd n

2229prettyName infixParen showNS bnd n

2146 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

2230 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

2147 | (UN n') <- n, T.unpack n' == "_" = text "_"

2231 | (UN n') <- n, T.unpack n' == "_" = text "_"

@@ -2228,11 +2312,11 @@ getAll = map getTm

2228

2312

2229

2313

2230-- | Show Idris name

2314-- | Show Idris name

2231−showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

2315+showName :: Maybe IState -- ^ the Idris state, for information about names and colours

2232− -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

2316+ -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit

2233− -> PPOption -- ^^ pretty printing options

2317+ -> PPOption -- ^ pretty printing options

2234− -> Bool -- ^^ whether to colourise

2318+ -> Bool -- ^ whether to colourise

2235− -> Name -- ^^ the term to show

2319+ -> Name -- ^ the term to show

2236 -> String

2320 -> String

2237showName ist bnd ppo colour n = case ist of

2321showName ist bnd ppo colour n = case ist of

2238 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

2322 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

@@ -2256,8 +2340,8 @@ showName ist bnd ppo colour n = case ist of

2256 -- (like error messages). Thus, unknown vars are colourised as implicits.

2340 -- (like error messages). Thus, unknown vars are colourised as implicits.

2257 | otherwise -> colouriseImplicit t name

2341 | otherwise -> colouriseImplicit t name

2258

2342

2259−showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

2343+showTm :: IState -- ^ the Idris state, for information about identifiers and colours

2260− -> PTerm -- ^^ the term to show

2344+ -> PTerm -- ^ the term to show

2261 -> String

2345 -> String

2262showTm ist = displayDecorated (consoleDecorate ist) .

2346showTm ist = displayDecorated (consoleDecorate ist) .

2263 renderPretty 0.8 100000 .

2347 renderPretty 0.8 100000 .

src/Idris/CaseSplit.hs+11−11

@@ -50,11 +50,11 @@ Always take the "more specific" argument when there is a discrepancy, i.e.

50names over '_', patterns over names, etc.

51-}

53−-- Given a variable to split, and a term application, return a list of

53+-- | Given a variable to split, and a term application, return a list

54−-- variable updates, paired with a flag to say whether the given update

54+-- of variable updates, paired with a flag to say whether the given

55−-- typechecks (False = impossible)

55+-- update typechecks (False = impossible) if the flag is 'False' the

56−-- if the flag is 'False' the splits should be output with the 'impossible'

56+-- splits should be output with the 'impossible' flag, otherwise they

57−-- flag, otherwise they should be output as normal

57+-- should be output as normal

58split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])

59split n t'

60 = do ist <- getIState

@@ -170,8 +170,8 @@ mergePat ist orig new t =

170 put (ms { namemap = ((n', n) : namemap ms) })

171 addNameMap _ = return ()

172

173−-- If any names are unified, make sure they stay unified. Always prefer

173+-- | If any names are unified, make sure they stay unified. Always

174−-- user provided name (first pattern)

174+-- prefer user provided name (first pattern)

175mergePat' ist (PPatvar fc n) new t

176 = mergePat' ist (PRef fc [] n) new t

177mergePat' ist old (PPatvar fc n) t

@@ -240,7 +240,7 @@ elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

240 i <- getIState

241 return (True, delab i tm))

242 (\e -> do i <- getIState

243− logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n"

243+ logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n"

244 ++ pshow i e

245 return (False, t))

246

@@ -352,7 +352,7 @@ replaceSplits l ups impossible

352 updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest

353

354 addBrackets tm | ' ' `elem` tm

355− , not (isPrefixOf "(" tm && isSuffixOf ")" tm)

355+ , not (isPrefixOf "(" tm && isSuffixOf ")" tm)

356 = "(" ++ tm ++ ")"

357 | otherwise = tm

358

@@ -373,14 +373,14 @@ nameRoot acc nm =

373

374-- Show a name for use in pattern definitions on the lhs

375showLHSName :: Name -> String

376−showLHSName n = let fn = show n in

376+showLHSName n = let fn = show n in

377 if any (flip elem opChars) fn

378 then "(" ++ fn ++ ")"

379 else fn

380

381-- Show a name for the purpose of generating a metavariable name on the rhs

382showRHSName :: Name -> String

383−showRHSName n = let fn = show n in

383+showRHSName n = let fn = show n in

384 if any (flip elem opChars) fn

385 then "op"

386 else fn

src/Idris/Chaser.hs+16−15

@@ -28,10 +28,9 @@ latest :: UTCTime -> [ModuleTree] -> UTCTime

28latest tm [] = tm

29latest tm (m : ms) = latest (max tm (mod_time m)) (ms ++ mod_deps m)

31−-- Given a module tree, return the list of files to be loaded. If any

31+-- | Given a module tree, return the list of files to be loaded. If

32−-- module has a descendent which needs reloading, return its source, otherwise

32+-- any module has a descendent which needs reloading, return its

33−-- return the IBC

33+-- source, otherwise return the IBC

34−

35getModuleFiles :: [ModuleTree] -> [IFileType]

34getModuleFiles :: [ModuleTree] -> [IFileType]

36getModuleFiles ts = nub $ execState (modList ts) [] where

35getModuleFiles ts = nub $ execState (modList ts) [] where

37 modList :: [ModuleTree] -> State [IFileType] ()

36 modList :: [ModuleTree] -> State [IFileType] ()

@@ -66,7 +65,7 @@ getModuleFiles ts = nub $ execState (modList ts) [] where

66 then getSrc x : updateToSrc path xs

65 then getSrc x : updateToSrc path xs

67 else x : updateToSrc path xs

66 else x : updateToSrc path xs

69−-- Strip quotes and the backslash escapes that Haskeline adds

68+-- | Strip quotes and the backslash escapes that Haskeline adds

70extractFileName :: String -> String

69extractFileName :: String -> String

71extractFileName ('"':xs) = takeWhile (/= '"') xs

70extractFileName ('"':xs) = takeWhile (/= '"') xs

72extractFileName ('\'':xs) = takeWhile (/= '\'') xs

71extractFileName ('\'':xs) = takeWhile (/= '\'') xs

@@ -80,10 +79,11 @@ getIModTime (IBC i _) = getModificationTime i

80getIModTime (IDR i) = getModificationTime i

79getIModTime (IDR i) = getModificationTime i

81getIModTime (LIDR i) = getModificationTime i

80getIModTime (LIDR i) = getModificationTime i

83−getImports :: [(FilePath, [ImportInfo])] -> [FilePath] ->

82+getImports :: [(FilePath, [ImportInfo])]

83+ -> [FilePath]

84− Idris [(FilePath, [ImportInfo])]

84+ -> Idris [(FilePath, [ImportInfo])]

85getImports acc [] = return acc

86−getImports acc (f : fs) = do

86+getImports acc (f : fs) = do

87 i <- getIState

88 let file = extractFileName f

89 ibcsd <- valIBCSubDir i

@@ -97,7 +97,7 @@ getImports acc (f : fs) = do

97 exist <- runIO $ doesFileExist parsef

98 if exist then do

99 src_in <- runIO $ readSource parsef

100− src <- if lit fp then tclift $ unlit parsef src_in

100+ src <- if lit fp then tclift $ unlit parsef src_in

101 else return src_in

102 (_, _, modules, _) <- parseImports parsef src

103 clearParserWarnings

@@ -113,18 +113,19 @@ getImports acc (f : fs) = do

113 fname (LIDR fn) = fn

114 fname (IBC _ src) = fname src

115

116−buildTree :: [FilePath] -> -- already guaranteed built

116+buildTree :: [FilePath] -- ^ already guaranteed built

117− [(FilePath, [ImportInfo])] -> -- import lists (don't reparse)

117+ -> [(FilePath, [ImportInfo])] -- ^ import lists (don't reparse)

118+ -> FilePath

118− FilePath -> Idris [ModuleTree]

119+ -> Idris [ModuleTree]

119buildTree built importlists fp = evalStateT (btree [] fp) []

120buildTree built importlists fp = evalStateT (btree [] fp) []

120 where

121 where

121− addFile :: FilePath -> [ModuleTree] ->

122+ addFile :: FilePath -> [ModuleTree] ->

122 StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]

123 StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]

123 addFile f m = do fs <- get

124 addFile f m = do fs <- get

124 put ((f, m) : fs)

125 put ((f, m) : fs)

125 return m

126 return m

126

127

127− btree :: [FilePath] -> FilePath ->

128+ btree :: [FilePath] -> FilePath ->

128 StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]

129 StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]

129 btree stk f =

130 btree stk f =

130 do i <- lift getIState

131 do i <- lift getIState

@@ -137,7 +138,7 @@ buildTree built importlists fp = evalStateT (btree [] fp) []

137 mt <- lift $ runIO $ getIModTime fp

138 mt <- lift $ runIO $ getIModTime fp

138 if (file `elem` built)

139 if (file `elem` built)

139 then return [MTree fp False mt []]

140 then return [MTree fp False mt []]

140− else if file `elem` stk then

141+ else if file `elem` stk then

141 do lift $ tclift $ tfail

142 do lift $ tclift $ tfail

142 (Msg $ "Cycle detected in imports: "

143 (Msg $ "Cycle detected in imports: "

143 ++ showSep " -> " (reverse (file : stk)))

144 ++ showSep " -> " (reverse (file : stk)))

src/Idris/Coverage.hs+22−25

@@ -101,7 +101,7 @@ genClauses fc n xs given

101 -- anything based on earlier values

102 genPH :: IState -> Type -> [Bool]

103 genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc

104− genPH ist ty = []

104+ genPH ist ty = []

105

106 notConcrete ist t | (P _ n _, args) <- unApply t,

107 not (isConName n (tt_ctxt ist)) = True

@@ -315,9 +315,8 @@ genAll i (addPH, args)

315upd :: t -> PArg' t -> PArg' t

316upd p' p = p { getTm = p' }

317

318−-- Check whether function and all descendants cover all cases (partial is

318+-- | Check whether function and all descendants cover all cases

319−-- okay, as long as it's due to recursion)

319+-- (partial is okay, as long as it's due to recursion)

320−

321checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

320checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

322checkAllCovering fc done top n | not (n `elem` done)

321checkAllCovering fc done top n | not (n `elem` done)

323 = do i <- get

322 = do i <- get

@@ -334,10 +333,10 @@ checkAllCovering fc done top n | not (n `elem` done)

334 x -> return () -- stop if total

333 x -> return () -- stop if total

335checkAllCovering _ _ _ _ = return ()

334checkAllCovering _ _ _ _ = return ()

336

335

337−-- | Check if, in a given group of type declarations mut_ns,

336+-- | Check if, in a given group of type declarations mut_ns, the

338−-- the constructor cn : ty is strictly positive,

337+-- constructor cn : ty is strictly positive, and update the context

339−-- and update the context accordingly

338+-- accordingly

340−checkPositive :: [Name] -- ^ the group of type declarations

339+checkPositive :: [Name] -- ^ the group of type declarations

341 -> (Name, Type) -- ^ the constructor

340 -> (Name, Type) -- ^ the constructor

342 -> Idris Totality

341 -> Idris Totality

343checkPositive mut_ns (cn, ty')

342checkPositive mut_ns (cn, ty')

@@ -368,8 +367,8 @@ checkPositive mut_ns (cn, ty')

368 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

367 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

369

368

370

369

371−-- | Calculate the totality of a function from its patterns.

370+-- | Calculate the totality of a function from its patterns. Either

372−-- Either follow the size change graph (if inductive) or check for

371+-- follow the size change graph (if inductive) or check for

373-- productivity (if coinductive)

372-- productivity (if coinductive)

374calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

373calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

375calcTotality fc n pats

374calcTotality fc n pats

@@ -508,7 +507,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

508 scgPat (lhs, rhs) = let lhs' = delazy lhs

507 scgPat (lhs, rhs) = let lhs' = delazy lhs

509 rhs' = delazy rhs

508 rhs' = delazy rhs

510 (f, pargs) = unApply (dePat lhs') in

509 (f, pargs) = unApply (dePat lhs') in

511− findCalls [] Toplevel (dePat rhs') (patvars lhs')

510+ findCalls [] Toplevel (dePat rhs') (patvars lhs')

512 (zip pargs [0..])

511 (zip pargs [0..])

513

512

514 findCalls cases Delayed ap@(P _ n _) pvs args

513 findCalls cases Delayed ap@(P _ n _) pvs args

@@ -526,7 +525,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

526 -- check under guarded constructors.

525 -- check under guarded constructors.

527 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

526 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

528 Guarded <- guarded,

527 Guarded <- guarded,

529− del == txt "Delay"

528+ del == txt "Delay"

530 = findCalls cases Delayed arg pvs pargs

529 = findCalls cases Delayed arg pvs pargs

531 | (P _ n _, args) <- unApply ap,

530 | (P _ n _, args) <- unApply ap,

532 Delayed <- guarded,

531 Delayed <- guarded,

@@ -536,7 +535,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

536 | (P _ n _, args) <- unApply ap,

535 | (P _ n _, args) <- unApply ap,

537 Delayed <- guarded,

536 Delayed <- guarded,

538 isConName n (tt_ctxt ist)

537 isConName n (tt_ctxt ist)

539− = -- Still under a 'Delay' and constructor guarded, so check

538+ = -- Still under a 'Delay' and constructor guarded, so check

540 -- just the arguments to the constructor, remaining Delayed

539 -- just the arguments to the constructor, remaining Delayed

541 concatMap (\x -> findCalls cases guarded x pvs pargs) args

540 concatMap (\x -> findCalls cases guarded x pvs pargs) args

542 | (P _ n _, args) <- unApply ap,

541 | (P _ n _, args) <- unApply ap,

@@ -551,7 +550,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

551 then findCallsCase (n : cases) guarded n args pvs pargs

550 then findCallsCase (n : cases) guarded n args pvs pargs

552 else []

551 else []

553 | (P _ n _, args) <- unApply ap

552 | (P _ n _, args) <- unApply ap

554− -- Ordinary call, not under a delay.

553+ -- Ordinary call, not under a delay.

555 -- If n is a constructor, set 'args' as Guarded

554 -- If n is a constructor, set 'args' as Guarded

556 = let nguarded = case guarded of

555 = let nguarded = case guarded of

557 Unguarded -> Unguarded

556 Unguarded -> Unguarded

@@ -579,20 +578,20 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

579 -- are okay for building the size change

578 -- are okay for building the size change

580 findCallsCase cases guarded n args pvs pargs

579 findCallsCase cases guarded n args pvs pargs

581 = case lookupDefExact n (tt_ctxt ist) of

580 = case lookupDefExact n (tt_ctxt ist) of

582− Just (CaseOp _ _ _ pats _ cd) ->

581+ Just (CaseOp _ _ _ pats _ cd) ->

583 concatMap (fccPat cases pvs pargs args guarded) (rights pats)

582 concatMap (fccPat cases pvs pargs args guarded) (rights pats)

584 Nothing -> []

583 Nothing -> []

585

584

586− fccPat cases pvs pargs args g (lhs, rhs)

585+ fccPat cases pvs pargs args g (lhs, rhs)

587 = let lhs' = delazy lhs

586 = let lhs' = delazy lhs

588 rhs' = delazy rhs

587 rhs' = delazy rhs

589− (f, pargs_case) = unApply (dePat lhs')

588+ (f, pargs_case) = unApply (dePat lhs')

590 -- pargs is a pair of a term, and the argument position that

589 -- pargs is a pair of a term, and the argument position that

591 -- term appears in. If any of the arguments to the case block

590 -- term appears in. If any of the arguments to the case block

592 -- are also on the lhs, we also want those patterns to appear

591 -- are also on the lhs, we also want those patterns to appear

593 -- in the parg list so that we'll spot patterns which are

592 -- in the parg list so that we'll spot patterns which are

594 -- smaller than then

593 -- smaller than then

595− newpargs = newPArg args pargs

594+ newpargs = newPArg args pargs

596 -- Now need to update the rhs of the case with the names in the

595 -- Now need to update the rhs of the case with the names in the

597 -- outer definition: In rhs', wherever we see what's in pargs_case,

596 -- outer definition: In rhs', wherever we see what's in pargs_case,

598 -- replace it with the corresponding thing in pargs

597 -- replace it with the corresponding thing in pargs

@@ -602,11 +601,11 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

602 findCalls cases g newrhs pvs pargs'

601 findCalls cases g newrhs pvs pargs'

603 where

602 where

604 doCaseSubs [] tm = tm

603 doCaseSubs [] tm = tm

605− doCaseSubs ((x, x') : cs) tm

604+ doCaseSubs ((x, x') : cs) tm

606 = doCaseSubs (subIn x x' cs) (substTerm x x' tm)

605 = doCaseSubs (subIn x x' cs) (substTerm x x' tm)

607−

606+

608 subIn x x' [] = []

607 subIn x x' [] = []

609− subIn x x' ((l, r) : cs)

608+ subIn x x' ((l, r) : cs)

610 = (substTerm x x' l, substTerm x x' r) : subIn x x' cs

609 = (substTerm x x' l, substTerm x x' r) : subIn x x' cs

611

610

612 addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'

611 addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'

@@ -639,7 +638,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

639 as == txt "assert_smaller" && arg == p

638 as == txt "assert_smaller" && arg == p

640 = Just (i, Smaller)

639 = Just (i, Smaller)

641 | smaller Nothing a (p, Nothing) = Just (i, Smaller)

640 | smaller Nothing a (p, Nothing) = Just (i, Smaller)

642− | otherwise = checkSize a ps

641+ | otherwise = checkSize a ps

643 checkSize a [] = Nothing

642 checkSize a [] = Nothing

644

643

645 -- the smaller thing we find must be defined in the same group of mutally

644 -- the smaller thing we find must be defined in the same group of mutally

@@ -692,7 +691,7 @@ checkSizeChange n = do

692 -- (Unchecked is okay as we'll spot problems here)

691 -- (Unchecked is okay as we'll spot problems here)

693 let tot = map (checkMP ist n (getArity ist n)) ms

692 let tot = map (checkMP ist n (getArity ist n)) ms

694 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"

693 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"

695− logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++

694+ logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++

696 (showSep "\n" (map show (zip ms tot)))

695 (showSep "\n" (map show (zip ms tot)))

697 return (noPartial tot)

696 return (noPartial tot)

698 [] -> do logCoverage 5 $ "No paths for " ++ show n

697 [] -> do logCoverage 5 $ "No paths for " ++ show n

@@ -826,5 +825,3 @@ totalityCheckBlock = do

826 mapM_ buildSCG (idris_totcheck ist)

825 mapM_ buildSCG (idris_totcheck ist)

827 mapM_ checkDeclTotality (idris_totcheck ist)

826 mapM_ checkDeclTotality (idris_totcheck ist)

828 clear_totcheck

827 clear_totcheck

829−

830−

src/Idris/DataOpts.hs+1−1

@@ -87,7 +87,7 @@ instance Optimisable (TT Name) where

87 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

88 applyOpts t = return t

90−-- Need to saturate arguments first to ensure that optimisation happens uniformly

90+-- | Need to saturate arguments first to ensure that optimisation happens uniformly

91applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term

92applyDataOptRT n tag arity uniq args

93 | length args == arity = doOpts n args

src/Idris/Elab/Class.hs+24−18

@@ -54,14 +54,20 @@ import Util.Pretty(pretty, text)

55data MArgTy = IA Name | EA Name | CA deriving Show

57+elabClass :: ElabInfo

58+ -> SyntaxInfo

57−elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

59+ -> Docstring (Either Err PTerm)

60+ -> FC

58− FC -> [(Name, PTerm)] ->

61+ -> [(Name, PTerm)]

62+ -> Name

63+ -> FC

64+ -> [(Name, FC, PTerm)]

59− Name -> FC -> [(Name, FC, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

65+ -> [(Name, Docstring (Either Err PTerm))]

60− [(Name, FC)] {- ^ determining params -} ->

66+ -> [(Name, FC)] -- ^ determining params

61− [PDecl] {- ^ class body -} ->

67+ -> [PDecl] -- ^ class body

62− Maybe (Name, FC) {- ^ instance ctor name and location -} ->

68+ -> Maybe (Name, FC) -- ^ instance ctor name and location

63− Docstring (Either Err PTerm) {- ^ instance ctor docs -} ->

69+ -> Docstring (Either Err PTerm) -- ^ instance ctor docs

64− Idris ()

70+ -> Idris ()

65elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

71elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

66 = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn)

72 = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn)

67 let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

73 let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

@@ -79,7 +85,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

79 mapM_ checkDefaultSuperclassInstance idecls

85 mapM_ checkDefaultSuperclassInstance idecls

80 let mnames = map getMName mdecls

86 let mnames = map getMName mdecls

81 ist <- getIState

87 ist <- getIState

82− let constraintNames = nub $

88+ let constraintNames = nub $

83 concatMap (namesIn [] ist) (map snd constraints)

89 concatMap (namesIn [] ist) (map snd constraints)

85 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames

91 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames

@@ -161,10 +167,10 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

161

167

162 checkConstraintName :: [Name] -> Name -> Idris ()

168 checkConstraintName :: [Name] -> Name -> Idris ()

163 checkConstraintName bound cname

169 checkConstraintName bound cname

164− | cname `notElem` bound

170+ | cname `notElem` bound

165− = tclift $ tfail (At fc (Msg $ "Name " ++ show cname ++

171+ = tclift $ tfail (At fc (Msg $ "Name " ++ show cname ++

166 " is not bound in interface " ++ show tn

172 " is not bound in interface " ++ show tn

167− ++ " " ++ showSep " " (map show bound)))

173+ ++ " " ++ showSep " " (map show bound)))

168 | otherwise = return ()

174 | otherwise = return ()

169

175

170 impbind :: [(Name, PTerm)] -> PTerm -> PTerm

176 impbind :: [(Name, PTerm)] -> PTerm -> PTerm

@@ -185,7 +191,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

185 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

191 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

186 (\ l s p -> Imp l s p Nothing True) t'))),

192 (\ l s p -> Imp l s p Nothing True) t'))),

187 (n, (nfc, syn, o, t) ) )

193 (n, (nfc, syn, o, t) ) )

188− tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

194+ tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

189 = do let o = []

195 = do let o = []

190 t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

196 t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

191 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

197 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

@@ -193,7 +199,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

193 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

199 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

194 (\ l s p -> Imp l s p Nothing True) t'))),

200 (\ l s p -> Imp l s p Nothing True) t'))),

195 (n, (nfc, syn, o, t) ) )

201 (n, (nfc, syn, o, t) ) )

196− tdecl allmeths (PData doc _ syn _ _ _)

202+ tdecl allmeths (PData doc _ syn _ _ _)

197 = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")

203 = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")

198 tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration")

204 tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration")

199

205

@@ -292,19 +298,19 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

292 -- Also ensure the dictionary is used for lookup of any methods that

298 -- Also ensure the dictionary is used for lookup of any methods that

293 -- are used in the type

299 -- are used in the type

294 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

300 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

295− insertConstraint c all sc

301+ insertConstraint c all sc

296− = let dictN = sMN 0 "__class" in

302+ = let dictN = sMN 0 "__class" in

297 PPi (constraint { pstatic = Static })

303 PPi (constraint { pstatic = Static })

298 dictN NoFC c

304 dictN NoFC c

299 (constrainMeths (map basename all)

305 (constrainMeths (map basename all)

300 dictN sc)

306 dictN sc)

301− where

307+ where

302 -- After we insert the constraint into the lookup, we need to

308 -- After we insert the constraint into the lookup, we need to

303 -- ensure that the same dictionary is used to resolve lookups

309 -- ensure that the same dictionary is used to resolve lookups

304 -- to the other methods in the class

310 -- to the other methods in the class

305 constrainMeths :: [Name] -> Name -> PTerm -> PTerm

311 constrainMeths :: [Name] -> Name -> PTerm -> PTerm

306 constrainMeths allM dictN tm = transform (addC allM dictN) tm

312 constrainMeths allM dictN tm = transform (addC allM dictN) tm

307−

313+

308 addC allM dictN m@(PRef fc hls n)

314 addC allM dictN m@(PRef fc hls n)

309 | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]

315 | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]

310 | otherwise = m

316 | otherwise = m

src/Idris/Elab/Clause.hs+8−8

@@ -512,7 +512,7 @@ findUnique ctxt env (Bind n b sc)

512 else findUnique ctxt ((n, b) : env) sc

513findUnique _ _ _ = []

514

515−-- Return the elaborated LHS/RHS, and the original LHS with implicits added

515+-- | Return the elaborated LHS/RHS, and the original LHS with implicits added

516elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

517 Idris (Either Term (Term, Term), PTerm)

518elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

@@ -554,7 +554,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

554

555 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

556 propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)

557−

557+

558-- let lhs = mkLHSapp $

559-- propagateParams i params fn_ty (addImplPat i lhs_in)

560 logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

@@ -704,7 +704,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

704 -- allow the deferred things to be definable

705 -- (this is just to allow users to inspect intermediate

706 -- things)

707− <- if (null holes || null def') && not inf

707+ <- if (null holes || null def') && not inf

708 then recheckC_borrowing True (PEGenerated `notElem` opts)

709 borrowed fc id [] rhs'

710 else return (rhs', clhsty)

@@ -1033,7 +1033,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1033 | otherwise = Placeholder

1034

1035 updateWithTerm :: IState -> Maybe Name -> Name -> PTerm -> [Name] -> [Name] -> PTerm -> PTerm

1036− updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1036+ updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1037 = mapPT updateApp tm

1038 where

1039 arity (PApp _ _ as) = length as

@@ -1097,18 +1097,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1097

1098 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)

1099

1100−-- Apply a transformation to all RHSes and nested RHSs

1100+-- | Apply a transformation to all RHSes and nested RHSs

1101mapRHS :: (PTerm -> PTerm) -> PClause -> PClause

1102−mapRHS f (PClause fc n lhs args rhs ws)

1102+mapRHS f (PClause fc n lhs args rhs ws)

1103 = PClause fc n lhs args (f rhs) (map (mapRHSdecl f) ws)

1104mapRHS f (PWith fc n lhs args warg prf ws)

1105 = PWith fc n lhs args (f warg) prf (map (mapRHSdecl f) ws)

1106−mapRHS f (PClauseR fc args rhs ws)

1106+mapRHS f (PClauseR fc args rhs ws)

1107 = PClauseR fc args (f rhs) (map (mapRHSdecl f) ws)

1108mapRHS f (PWithR fc args warg prf ws)

1109 = PWithR fc args (f warg) prf (map (mapRHSdecl f) ws)

1110

1111mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl

1112−mapRHSdecl f (PClauses fc opt n cs)

1112+mapRHSdecl f (PClauses fc opt n cs)

1113 = PClauses fc opt n (map (mapRHS f) cs)

1114mapRHSdecl f t = t

src/Idris/Elab/Instance.hs+44−42

@@ -50,21 +50,24 @@ import Data.List.Split (splitOn)

51import Util.Pretty(pretty, text)

53−elabInstance :: ElabInfo -> SyntaxInfo ->

53+elabInstance :: ElabInfo

54+ -> SyntaxInfo

54− Docstring (Either Err PTerm) ->

55+ -> Docstring (Either Err PTerm)

55− [(Name, Docstring (Either Err PTerm))] ->

56+ -> [(Name, Docstring (Either Err PTerm))]

56− ElabWhat -> -- phase

57+ -> ElabWhat -- ^ phase

58+ -> FC

57− FC -> [(Name, PTerm)] -> -- constraints

59+ -> [(Name, PTerm)] -- ^ constraints

58− [Name] -> -- parent dictionary names (optionally)

60+ -> [Name] -- ^ parent dictionary names (optionally)

59− Accessibility ->

61+ -> Accessibility

60− FnOpts ->

62+ -> FnOpts

61− Name -> -- the class

63+ -> Name -- ^ the class

62− FC -> -- precise location of class name

64+ -> FC -- ^ precise location of class name

63− [PTerm] -> -- class parameters (i.e. instance)

65+ -> [PTerm] -- ^ class parameters (i.e. instance)

64− [(Name, PTerm)] -> -- Extra arguments in scope (e.g. instance in where block)

66+ -> [(Name, PTerm)] -- ^ Extra arguments in scope (e.g. instance in where block)

65− PTerm -> -- full instance type

67+ -> PTerm -- ^ full instance type

66− Maybe Name -> -- explicit name

68+ -> Maybe Name -- ^ explicit name

67− [PDecl] -> Idris ()

69+ -> [PDecl]

70+ -> Idris ()

68elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do

71elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do

69 ist <- getIState

72 ist <- getIState

70 (n, ci) <- case lookupCtxtName n (idris_classes ist) of

73 (n, ci) <- case lookupCtxtName n (idris_classes ist) of

@@ -81,7 +84,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

82 let emptyclass = null (class_methods ci)

85 let emptyclass = null (class_methods ci)

83 when (what /= EDefns) $ do

86 when (what /= EDefns) $ do

84− nty <- elabType' True info syn doc argDocs fc totopts iname NoFC

87+ nty <- elabType' True info syn doc argDocs fc totopts iname NoFC

85 (piBindp expl_param pextra t)

88 (piBindp expl_param pextra t)

86 -- if the instance type matches any of the instances we have already,

89 -- if the instance type matches any of the instances we have already,

87 -- and it's not a named instance, then it's overlapping, so report an error

90 -- and it's not a named instance, then it's overlapping, so report an error

@@ -111,7 +114,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

111 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

114 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

112 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

115 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

113 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

116 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

114−

117+

115 ist <- getIState

118 ist <- getIState

116 -- Bring variables in instance head into scope when building the

119 -- Bring variables in instance head into scope when building the

117 -- dictionary

120 -- dictionary

@@ -121,11 +124,11 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

121 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)

124 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)

122 _ -> (zip headVars (repeat Placeholder), Erased)

125 _ -> (zip headVars (repeat Placeholder), Erased)

123 logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

126 logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

124−

127+

125 let all_meths = map (nsroot . fst) (class_methods ci)

128 let all_meths = map (nsroot . fst) (class_methods ci)

126 let mtys = map (\ (n, (inj, op, t)) ->

129 let mtys = map (\ (n, (inj, op, t)) ->

127 let t_in = substMatchesShadow ips pnames t

130 let t_in = substMatchesShadow ips pnames t

128− mnamemap =

131+ mnamemap =

129 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

132 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

130 (map (toImp fc) headVars)))

133 (map (toImp fc) headVars)))

131 all_meths

134 all_meths

@@ -182,13 +185,13 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

182 Nothing -> []

185 Nothing -> []

183 let prop_params = getParamsInType ist [] ifn_is ifn_ty

186 let prop_params = getParamsInType ist [] ifn_is ifn_ty

184

187

185− logElab 3 $ "Propagating parameters to methods: "

188+ logElab 3 $ "Propagating parameters to methods: "

186 ++ show (iname, prop_params)

189 ++ show (iname, prop_params)

187

190

188 let wbVals' = map (addParams prop_params) wbVals

191 let wbVals' = map (addParams prop_params) wbVals

189

192

190 mapM_ (rec_elabDecl info EAll info) wbVals'

193 mapM_ (rec_elabDecl info EAll info) wbVals'

191−

194+

192 mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')

195 mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')

193

196

194 pop_estack

197 pop_estack

@@ -212,8 +215,8 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

212 Just nm -> nm

215 Just nm -> nm

213

216

214 substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)

217 substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)

215− = PInstance doc argDocs syn fc cs parents acc opts n nfc

218+ = PInstance doc argDocs syn fc cs parents acc opts n nfc

216− (map (substMatchesShadow ips pnames) ps)

219+ (map (substMatchesShadow ips pnames) ps)

217 pextra

220 pextra

218 (substMatchesShadow ips pnames t) expn ds

221 (substMatchesShadow ips pnames t) expn ds

219

222

@@ -275,10 +278,10 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

275 keepDets dets t = t

278 keepDets dets t = t

276

279

277 methName (n, _, _, _) = n

280 methName (n, _, _, _) = n

278− toExp n = pexp (PRef fc [] n)

281+ toExp n = pexp (PRef fc [] n)

279

282

280− mkMethApp ps (n, _, _, ty)

283+ mkMethApp ps (n, _, _, ty)

281− = lamBind 0 ty (papp fc (PRef fc [] n)

284+ = lamBind 0 ty (papp fc (PRef fc [] n)

282 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

285 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

283 where

286 where

284 needed is p = pname p `elem` map pname is

287 needed is p = pname p `elem` map pname is

@@ -311,7 +314,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

311

314

312 decorate ns iname (NS (UN nm) s)

315 decorate ns iname (NS (UN nm) s)

313 = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns

316 = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns

314− decorate ns iname nm

317+ decorate ns iname nm

315 = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns

318 = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns

316

319

317 mkTyDecl (n, op, t, _)

320 mkTyDecl (n, op, t, _)

@@ -375,7 +378,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

375 clauseFor m iname ns (PClauses _ _ m' _)

378 clauseFor m iname ns (PClauses _ _ m' _)

376 = decorate ns iname m == decorate ns iname m'

379 = decorate ns iname m == decorate ns iname m'

377 clauseFor m iname ns _ = False

380 clauseFor m iname ns _ = False

378−

381+

379getHeadVars :: PTerm -> [Name]

382getHeadVars :: PTerm -> [Name]

380getHeadVars (PRef _ _ n) | implicitable n = [n]

383getHeadVars (PRef _ _ n) | implicitable n = [n]

381getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)

384getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)

@@ -383,14 +386,14 @@ getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r

383getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t

386getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t

384getHeadVars _ = []

387getHeadVars _ = []

385

388

386−-- Implicitly bind variables from the instance head in method types

389+-- | Implicitly bind variables from the instance head in method types

387impBind :: [(Name, PTerm)] -> PDecl -> PDecl

390impBind :: [(Name, PTerm)] -> PDecl -> PDecl

388impBind vs (PTy d ds syn fc opts n fc' t)

391impBind vs (PTy d ds syn fc opts n fc' t)

389− = PTy d ds syn fc opts n fc'

392+ = PTy d ds syn fc opts n fc'

390 (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)

393 (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)

391 where

394 where

392 doImpBind [] ty = ty

395 doImpBind [] ty = ty

393− doImpBind ((n, argty) : ns) ty

396+ doImpBind ((n, argty) : ns) ty

394 = PPi impl n NoFC argty (doImpBind ns ty)

397 = PPi impl n NoFC argty (doImpBind ns ty)

395

398

396 boundIn (PPi _ n _ _ sc) = n : boundIn sc

399 boundIn (PPi _ n _ _ sc) = n : boundIn sc

@@ -404,19 +407,19 @@ getTypeIn ist n tm = Placeholder

404

407

405toImp fc n = pimp n (PRef fc [] n) True

408toImp fc n = pimp n (PRef fc [] n) True

406

409

407−-- Propagate class parameters to method bodies, if they're not already

410+-- | Propagate class parameters to method bodies, if they're not

408−-- there, and they are needed (i.e. appear in method's type)

411+-- already there, and they are needed (i.e. appear in method's type)

409addParams :: [Name] -> PDecl -> PDecl

412addParams :: [Name] -> PDecl -> PDecl

410addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

413addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

411 where

414 where

412 addCParams (PClause fc n lhs ws rhs wb)

415 addCParams (PClause fc n lhs ws rhs wb)

413 = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb

416 = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb

414 addCParams (PWith fc n lhs ws sc pn ds)

417 addCParams (PWith fc n lhs ws sc pn ds)

415− = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn

418+ = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn

416 (map (addParams ps) ds)

419 (map (addParams ps) ds)

417 addCParams c = c

420 addCParams c = c

418

421

419− addTmParams ps (PRef fc hls n)

422+ addTmParams ps (PRef fc hls n)

420 = PApp fc (PRef fc hls n) (map (toImp fc) ps)

423 = PApp fc (PRef fc hls n) (map (toImp fc) ps)

421 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)

424 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)

422 = PApp fc ap (mergePs (map (toImp fc) ps) args)

425 = PApp fc ap (mergePs (map (toImp fc) ps) args)

@@ -439,11 +442,10 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

439

442

440addParams ps d = d

443addParams ps d = d

441

444

442−-- Check a given method definition is injective, if the class info

445+-- | Check a given method definition is injective, if the class info

443−-- says it needs to be.

444−-- Takes originally written decl and the one with name decoration, so

446+-- says it needs to be. Takes originally written decl and the one

445−-- we know which name to look up.

447+-- with name decoration, so we know which name to look up.

446−checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->

448+checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->

447 (PDecl, PDecl) -> Idris ()

449 (PDecl, PDecl) -> Idris ()

448checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)

450checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)

449 | Just (True, _, _) <- clookup n ns

451 | Just (True, _, _) <- clookup n ns

@@ -452,13 +454,13 @@ checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)

452 Just (CaseOp _ _ _ _ _ cdefs) ->

454 Just (CaseOp _ _ _ _ _ cdefs) ->

453 checkInjectiveCase ist (snd (cases_compiletime cdefs))

455 checkInjectiveCase ist (snd (cases_compiletime cdefs))

454 where

456 where

455− checkInjectiveCase ist (STerm tm)

457+ checkInjectiveCase ist (STerm tm)

456 = checkInjectiveApp ist (fst (unApply tm))

458 = checkInjectiveApp ist (fst (unApply tm))

457 checkInjectiveCase _ _ = notifail

459 checkInjectiveCase _ _ = notifail

458

460

459 checkInjectiveApp ist (P (TCon _ _) n _) = return ()

461 checkInjectiveApp ist (P (TCon _ _) n _) = return ()

460 checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()

462 checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()

461− checkInjectiveApp ist (P Ref n _)

463+ checkInjectiveApp ist (P Ref n _)

462 | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()

464 | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()

463 checkInjectiveApp ist (P Ref n _) = notifail

465 checkInjectiveApp ist (P Ref n _) = notifail

464 checkInjectiveApp _ _ = notifail

466 checkInjectiveApp _ _ = notifail

src/Idris/Elab/Record.hs+38−34

@@ -35,16 +35,18 @@ import Control.Monad

35-- | Elaborate a record declaration

36elabRecord :: ElabInfo

37 -> ElabWhat

38− -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

38+ -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

39− -> SyntaxInfo -> FC -> DataOpts

39+ -> SyntaxInfo

40+ -> FC

41+ -> DataOpts

40− -> Name -- ^ The name of the type being defined

42+ -> Name -- ^ The name of the type being defined

41− -> FC -- ^ The precise source location of the tycon name

43+ -> FC -- ^ The precise source location of the tycon name

42− -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters

44+ -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters

43− -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs

45+ -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs

44 -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields

46 -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields

45− -> Maybe (Name, FC) -- ^ Constructor Name

47+ -> Maybe (Name, FC) -- ^ Constructor Name

46− -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

48+ -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

47− -> SyntaxInfo -- ^ Constructor SyntaxInfo

49+ -> SyntaxInfo -- ^ Constructor SyntaxInfo

48 -> Idris ()

50 -> Idris ()

49elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

51elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

50 = do logElab 1 $ "Building data declaration for " ++ show tyn

52 = do logElab 1 $ "Building data declaration for " ++ show tyn

@@ -154,12 +156,14 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc

154 in (n, nfc, p, t, doc) : (fwnad rest)

156 in (n, nfc, p, t, doc) : (fwnad rest)

155 fwnad [] = []

157 fwnad [] = []

156

158

157−elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC

159+elabRecordFunctions :: ElabInfo

160+ -> SyntaxInfo

161+ -> FC

158− -> Name -- ^ Record type name

162+ -> Name -- ^ Record type name

159 -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters

163 -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters

160 -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields

164 -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields

161− -> Name -- ^ Constructor Name

165+ -> Name -- ^ Constructor Name

162− -> PTerm -- ^ Target type

166+ -> PTerm -- ^ Target type

163 -> Idris ()

167 -> Idris ()

164elabRecordFunctions info rsyn fc tyn params fields dconName target

168elabRecordFunctions info rsyn fc tyn params fields dconName target

165 = do logElab 1 $ "Elaborating helper functions for record " ++ show tyn

169 = do logElab 1 $ "Elaborating helper functions for record " ++ show tyn

@@ -301,17 +305,17 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

301

305

302-- | Creates and elaborates a projection function.

306-- | Creates and elaborates a projection function.

303elabProjection :: ElabInfo

307elabProjection :: ElabInfo

304− -> Name -- ^ Name of the argument in the constructor

308+ -> Name -- ^ Name of the argument in the constructor

305− -> Name -- ^ Projection Name

309+ -> Name -- ^ Projection Name

306− -> Plicity -- ^ Projection Plicity

310+ -> Plicity -- ^ Projection Plicity

307− -> PTerm -- ^ Projection Type

311+ -> PTerm -- ^ Projection Type

308 -> (Docstring (Either Err PTerm)) -- ^ Projection Documentation

312 -> (Docstring (Either Err PTerm)) -- ^ Projection Documentation

309− -> SyntaxInfo -- ^ Projection SyntaxInfo

313+ -> SyntaxInfo -- ^ Projection SyntaxInfo

310− -> FC -> PTerm -- ^ Projection target type

314+ -> FC -> PTerm -- ^ Projection target type

311− -> Name -- ^ Data constructor tame

315+ -> Name -- ^ Data constructor tame

312− -> [PArg] -- ^ Placeholder Arguments to constructor

316+ -> [PArg] -- ^ Placeholder Arguments to constructor

313− -> [Name] -- ^ All Field Names

317+ -> [Name] -- ^ All Field Names

314− -> Int -- ^ Argument Index

318+ -> Int -- ^ Argument Index

315 -> Idris ()

319 -> Idris ()

316elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

320elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

317 = do logElab 1 $ "Generating Projection for " ++ show pname

321 = do logElab 1 $ "Generating Projection for " ++ show pname

@@ -358,18 +362,18 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f

358-- | Creates and elaborates an update function.

362-- | Creates and elaborates an update function.

359-- If 'optional' is true, we will not fail if we can't elaborate the update function.

363-- If 'optional' is true, we will not fail if we can't elaborate the update function.

360elabUpdate :: ElabInfo

364elabUpdate :: ElabInfo

361− -> Name -- ^ Name of the argument in the constructor

365+ -> Name -- ^ Name of the argument in the constructor

362− -> Name -- ^ Field Name

366+ -> Name -- ^ Field Name

363− -> Plicity -- ^ Field Plicity

367+ -> Plicity -- ^ Field Plicity

364− -> PTerm -- ^ Field Type

368+ -> PTerm -- ^ Field Type

365 -> (Docstring (Either Err PTerm)) -- ^ Field Documentation

369 -> (Docstring (Either Err PTerm)) -- ^ Field Documentation

366− -> SyntaxInfo -- ^ Field SyntaxInfo

370+ -> SyntaxInfo -- ^ Field SyntaxInfo

367− -> FC -> PTerm -- ^ Projection Source Type

371+ -> FC -> PTerm -- ^ Projection Source Type

368− -> Name -- ^ Data Constructor Name

372+ -> Name -- ^ Data Constructor Name

369− -> [PArg] -- ^ Arguments to constructor

373+ -> [PArg] -- ^ Arguments to constructor

370− -> [Name] -- ^ All fields

374+ -> [Name] -- ^ All fields

371− -> Int -- ^ Argument Index

375+ -> Int -- ^ Argument Index

372− -> Bool -- ^ Optional

376+ -> Bool -- ^ Optional

373 -> Idris ()

377 -> Idris ()

374elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

378elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

375 = do logElab 1 $ "Generating Update for " ++ show pname

379 = do logElab 1 $ "Generating Update for " ++ show pname

src/Idris/Elab/Rewrite.hs+27−27

@@ -17,7 +17,7 @@ import Data.List

18import Debug.Trace

20−elabRewrite :: (PTerm -> ElabD ()) -> IState ->

20+elabRewrite :: (PTerm -> ElabD ()) -> IState ->

21 FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

22-- Old version, no rewrite rule given

23{-

@@ -47,7 +47,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

47 Nothing -> return sc_in

48 Just t -> do

49 letn <- getNameFrom (sMN 0 "rewrite_result")

50− return $ PLet fc letn fc t sc_in

50+ return $ PLet fc letn fc t sc_in

51 (PRef fc [] letn)

52 tyn <- getNameFrom (sMN 0 "rty")

53 claim tyn RType

@@ -75,7 +75,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

75 [pexp pred, pexp rule, pexp sc])

76-- trace ("LHS: " ++ show l ++ "\n" ++

77-- "RHS: " ++ show r ++ "\n" ++

78−-- "REWRITE: " ++ show rewrite ++ "\n" ++

78+-- "REWRITE: " ++ show rewrite ++ "\n" ++

79-- "GOAL: " ++ show (delab ist g)) $

80 elab rewrite

81 solve

@@ -84,7 +84,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

84 mkP :: TT Name -> -- Left term, top level

85 TT Name -> TT Name -> TT Name -> TT Name

86 mkP lt l r ty | l == ty = lt

87− mkP lt l r (App s f a)

87+ mkP lt l r (App s f a)

88 = let f' = if (r /= f) then mkP lt l r f else f

89 a' = if (r /= a) then mkP lt l r a else a in

90 App s f' a'

@@ -101,7 +101,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

101 mkP lt l r x = x

102

103 -- If we're rewriting a dependent type, the rewrite type the rewrite

104− -- may break the indices.

104+ -- may break the indices.

105 -- So, for any function argument which can be determined by looking

106 -- at the indices (i.e. any constructor guarded elsewhere in the type)

107 -- replace it with a _. e.g. (++) a n m xs ys becomes (++) _ _ _ xs ys

@@ -116,7 +116,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

116 where removeImp tm@(PImp{}) = tm { getTm = Placeholder }

117 removeImp t = t

118 phApps tm = tm

119−

119+

120findSubstFn :: Maybe Name -> IState -> Type -> Type -> ElabD Name

121findSubstFn Nothing ist lt rt

122 | lt == rt = return (sUN "rewrite__impl")

@@ -129,8 +129,8 @@ findSubstFn Nothing ist lt rt

129 Just _ -> return (rewrite_name lcon)

130 Nothing -> rewriteFail lt rt

131 | otherwise = rewriteFail lt rt

132− where rewriteFail lt rt = lift . tfail .

132+ where rewriteFail lt rt = lift . tfail .

133− Msg $ "Can't rewrite heterogeneous equality on types " ++

133+ Msg $ "Can't rewrite heterogeneous equality on types " ++

134 show (delab ist lt) ++ " and " ++ show (delab ist rt)

135

136findSubstFn (Just substfn_in) ist lt rt

@@ -142,8 +142,8 @@ findSubstFn (Just substfn_in) ist lt rt

142rewrite_name :: Name -> Name

143rewrite_name n = sMN 0 (show n ++ "_rewrite_lemma")

144

145−data ParamInfo = Index

145+data ParamInfo = Index

146− | Param

146+ | Param

147 | ImplicitIndex

148 | ImplicitParam

149 deriving Show

@@ -163,9 +163,11 @@ isParam Param = True

163isParam ImplicitIndex = False

164isParam ImplicitParam = True

165

166−-- Make a rewriting lemma for the given type constructor.

166+-- | Make a rewriting lemma for the given type constructor.

167+--

167−-- If it fails, fail silently (it may well fail for some very complex types.

168+-- If it fails, fail silently (it may well fail for some very complex

168−-- We can fix this later, for now this gives us a lot more working rewrites...)

169+-- types. We can fix this later, for now this gives us a lot more

170+-- working rewrites...)

169elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris ()

171elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris ()

170elabRewriteLemma info n cty_in =

172elabRewriteLemma info n cty_in =

171 do ist <- getIState

173 do ist <- getIState

@@ -176,7 +178,7 @@ elabRewriteLemma info n cty_in =

176 Just ti -> do

178 Just ti -> do

177 let imps = case lookupCtxtExact n (idris_implicits ist) of

179 let imps = case lookupCtxtExact n (idris_implicits ist) of

178 Nothing -> repeat (pexp Placeholder)

180 Nothing -> repeat (pexp Placeholder)

179− Just is -> is

181+ Just is -> is

180 let pinfo = getParamInfo cty imps 0 (param_pos ti)

182 let pinfo = getParamInfo cty imps 0 (param_pos ti)

181 if all isParam pinfo

183 if all isParam pinfo

182 then return () -- no need for a lemma, = will be homogeneous

184 then return () -- no need for a lemma, = will be homogeneous

@@ -189,7 +191,7 @@ mkLemma info lemma tcon ps ty =

189 let leftty = mkTy tcon ps (namesFrom "p" 0) (namesFrom "left" 0)

191 let leftty = mkTy tcon ps (namesFrom "p" 0) (namesFrom "left" 0)

190 rightty = mkTy tcon ps (namesFrom "p" 0) (namesFrom "right" 0)

192 rightty = mkTy tcon ps (namesFrom "p" 0) (namesFrom "right" 0)

191 predty = bindIdxs ist ps ty (namesFrom "pred" 0) $

193 predty = bindIdxs ist ps ty (namesFrom "pred" 0) $

192− PPi expl (sMN 0 "rep") fc

194+ PPi expl (sMN 0 "rep") fc

193 (mkTy tcon ps (namesFrom "p" 0) (namesFrom "pred" 0))

195 (mkTy tcon ps (namesFrom "p" 0) (namesFrom "pred" 0))

194 (PType fc)

196 (PType fc)

195 let xarg = sMN 0 "x"

197 let xarg = sMN 0 "x"

@@ -215,8 +217,8 @@ mkLemma info lemma tcon ps ty =

215 let lemRHS = PRef fc [] prop

217 let lemRHS = PRef fc [] prop

216

218

217 -- Elaborate the type of the lemma

219 -- Elaborate the type of the lemma

218− rec_elabDecl info EAll info

220+ rec_elabDecl info EAll info

219− (PTy emptyDocstring [] defaultSyntax fc [] lemma fc lemTy)

221+ (PTy emptyDocstring [] defaultSyntax fc [] lemma fc lemTy)

220 -- Elaborate the definition

222 -- Elaborate the definition

221 rec_elabDecl info EAll info

223 rec_elabDecl info EAll info

222 (PClauses fc [] lemma [PClause fc lemma lemLHS [] lemRHS []])

224 (PClauses fc [] lemma [PClause fc lemma lemLHS [] lemRHS []])

@@ -224,9 +226,9 @@ mkLemma info lemma tcon ps ty =

224 where

226 where

225 fc = emptyFC

227 fc = emptyFC

226

228

227− namesFrom x i = sMN i x : namesFrom x (i + 1)

229+ namesFrom x i = sMN i x : namesFrom x (i + 1)

228−

230+

229− mkTy fn pinfo ps is

231+ mkTy fn pinfo ps is

230 = PApp fc (PRef fc [] fn) (mkArgs pinfo ps is)

232 = PApp fc (PRef fc [] fn) (mkArgs pinfo ps is)

231

233

232 mkArgs [] ps is = []

234 mkArgs [] ps is = []

@@ -241,15 +243,13 @@ mkLemma info lemma tcon ps ty =

241 mkArgs _ _ _ = []

243 mkArgs _ _ _ = []

242

244

243 bindIdxs ist [] ty is tm = tm

245 bindIdxs ist [] ty is tm = tm

244− bindIdxs ist (Param : pinfo) (Bind n (Pi _ ty _) sc) is tm

246+ bindIdxs ist (Param : pinfo) (Bind n (Pi _ ty _) sc) is tm

245 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

247 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

246− bindIdxs ist (Index : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm

248+ bindIdxs ist (Index : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm

247− = PPi forall_imp i fc (delab ist ty)

249+ = PPi forall_imp i fc (delab ist ty)

248 (bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm)

250 (bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm)

249− bindIdxs ist (ImplicitParam : pinfo) (Bind n (Pi _ ty _) sc) is tm

251+ bindIdxs ist (ImplicitParam : pinfo) (Bind n (Pi _ ty _) sc) is tm

250 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

252 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

251− bindIdxs ist (ImplicitIndex : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm

253+ bindIdxs ist (ImplicitIndex : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm

252 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

254 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

253 bindIdxs _ _ _ _ tm = tm

255 bindIdxs _ _ _ _ tm = tm

254−

255−

src/Idris/Elab/Term.hs+48−36

@@ -42,33 +42,38 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

42 deriving Eq

45−data ElabResult =

45+data ElabResult = ElabResult {

46+ -- | The term resulting from elaboration

46− ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

47+ resultTerm :: Term

48+ -- | Information about new metavariables

47− , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

49+ , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

48− -- ^ Information about new metavariables

49− , resultCaseDecls :: [PDecl]

50− -- ^ Deferred declarations as the meaning of case blocks

50+ -- | Deferred declarations as the meaning of case blocks

51− , resultContext :: Context

51+ , resultCaseDecls :: [PDecl]

52− -- ^ The potentially extended context from new definitions

52+ -- | The potentially extended context from new definitions

53− , resultTyDecls :: [RDeclInstructions]

53+ , resultContext :: Context

54− -- ^ Meta-info about the new type declarations

54+ -- | Meta-info about the new type declarations

55+ , resultTyDecls :: [RDeclInstructions]

56+ -- | Saved highlights from elaboration

55− , resultHighlighting :: [(FC, OutputAnnotation)]

57+ , resultHighlighting :: [(FC, OutputAnnotation)]

56− -- ^ Saved highlights from elaboration

57− , resultName :: Int

58− -- ^ The new global name counter

58+ -- | The new global name counter

59+ , resultName :: Int

59− }

60+ }

60−

61+

61−

62+

62−-- Using the elaborator, convert a term in raw syntax to a fully

63+-- | Using the elaborator, convert a term in raw syntax to a fully

63-- elaborated, typechecked term.

64-- elaborated, typechecked term.

64--

65--

65-- If building a pattern match, we convert undeclared variables from

66-- If building a pattern match, we convert undeclared variables from

66-- holes to pattern bindings.

67-- holes to pattern bindings.

67−

68+--

68-- Also find deferred names in the term and their types

69-- Also find deferred names in the term and their types

69−

70−build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

70+build :: IState

71+ -> ElabInfo

72+ -> ElabMode

73+ -> FnOpts

74+ -> Name

75+ -> PTerm

71− ElabD ElabResult

76+ -> ElabD ElabResult

72build ist info emode opts fn tm

77build ist info emode opts fn tm

73 = do elab ist info emode opts fn tm

78 = do elab ist info emode opts fn tm

74 let tmIn = tm

79 let tmIn = tm

@@ -139,7 +144,8 @@ build ist info emode opts fn tm

139 (h: hs) -> do patvar h; mkPat

144 (h: hs) -> do patvar h; mkPat

140 [] -> return ()

145 [] -> return ()

141

146

142−-- Build a term autogenerated as a typeclass method definition

147+-- | Build a term autogenerated as a typeclass method definition.

148+--

143-- (Separate, so we don't go overboard resolving things that we don't

149-- (Separate, so we don't go overboard resolving things that we don't

144-- know about yet on the LHS of a pattern def)

150-- know about yet on the LHS of a pattern def)

145

151

@@ -177,9 +183,10 @@ buildTC ist info emode opts fn ns tm

177 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

183 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

178 where pattern = emode == ELHS

184 where pattern = emode == ELHS

179

185

180−-- return whether arguments of the given constructor name can be

186+-- | return whether arguments of the given constructor name can be

181−-- matched on. If they're polymorphic, no, unless the type has beed made

187+-- matched on. If they're polymorphic, no, unless the type has beed

182−-- concrete by the time we get around to elaborating the argument.

188+-- made concrete by the time we get around to elaborating the

189+-- argument.

183getUnmatchable :: Context -> Name -> [Bool]

190getUnmatchable :: Context -> Name -> [Bool]

184getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

191getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

185 = case lookupTyExact n ctxt of

192 = case lookupTyExact n ctxt of

@@ -220,8 +227,13 @@ goal_polymorphic =

220-- | Returns the set of declarations we need to add to complete the

227-- | Returns the set of declarations we need to add to complete the

221-- definition (most likely case blocks to elaborate) as well as

228-- definition (most likely case blocks to elaborate) as well as

222-- declarations resulting from user tactic scripts (%runElab)

229-- declarations resulting from user tactic scripts (%runElab)

223−elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

230+elab :: IState

231+ -> ElabInfo

232+ -> ElabMode

233+ -> FnOpts

234+ -> Name

235+ -> PTerm

224− ElabD ()

236+ -> ElabD ()

225elab ist info emode opts fn tm

237elab ist info emode opts fn tm

226 = do let loglvl = opt_logLevel (idris_options ist)

238 = do let loglvl = opt_logLevel (idris_options ist)

227 when (loglvl > 5) $ unifyLog True

239 when (loglvl > 5) $ unifyLog True

@@ -1438,7 +1450,7 @@ elab ist info emode opts fn tm

1438 return (mkPApp fc a ftm args)

1450 return (mkPApp fc a ftm args)

1439 _ -> return tm

1451 _ -> return tm

1440 expandToArity t = return t

1452 expandToArity t = return t

1441−

1453+

1442 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1454 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1443 fullApp x = x

1455 fullApp x = x

1444

1456

@@ -1550,11 +1562,11 @@ elab ist info emode opts fn tm

1550 addAutoBind _ _ = return ()

1562 addAutoBind _ _ = return ()

1551

1563

1552 testImplicitWarning :: FC -> Name -> Type -> ElabD ()

1564 testImplicitWarning :: FC -> Name -> Type -> ElabD ()

1553− testImplicitWarning fc n goal

1565+ testImplicitWarning fc n goal

1554 | implicitable n && emode == ETyDecl

1566 | implicitable n && emode == ETyDecl

1555 = do env <- get_env

1567 = do env <- get_env

1556 est <- getAux

1568 est <- getAux

1557− when (n `elem` auto_binds est) $

1569+ when (n `elem` auto_binds est) $

1558 tryUnify env (lookupTyName n (tt_ctxt ist))

1570 tryUnify env (lookupTyName n (tt_ctxt ist))

1559 | otherwise = return ()

1571 | otherwise = return ()

1560 where

1572 where

@@ -1564,7 +1576,7 @@ elab ist info emode opts fn tm

1564 hs <- get_holes

1576 hs <- get_holes

1565 case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)

1577 case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)

1566 inj hs [] [] of

1578 inj hs [] [] of

1567− OK _ ->

1579+ OK _ ->

1568 updateAux (\est -> est { implicit_warnings =

1580 updateAux (\est -> est { implicit_warnings =

1569 (fc, nm) : implicit_warnings est })

1581 (fc, nm) : implicit_warnings est })

1570 _ -> tryUnify env ts

1582 _ -> tryUnify env ts

@@ -1645,7 +1657,7 @@ pruneByType env (P _ n _) goalty ist as

1645 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1657 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1646 case lookupTyExact f' ctxt of

1658 case lookupTyExact f' ctxt of

1647 Just ty -> case unApply (getRetTy ty) of

1659 Just ty -> case unApply (getRetTy ty) of

1648− (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)

1660+ (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)

1649 -> False

1661 -> False

1650 _ -> let ty' = normalise ctxt [] ty in

1662 _ -> let ty' = normalise ctxt [] ty in

1651-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $

1663-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $

@@ -1661,12 +1673,12 @@ pruneByType env (P _ n _) goalty ist as

1661 _ -> False

1673 _ -> False

1662

1674

1663 -- If the goal is a constructor, it must match the suggested function type

1675 -- If the goal is a constructor, it must match the suggested function type

1664− matching (P _ ctyn _) (P _ n' _)

1676+ matching (P _ ctyn _) (P _ n' _)

1665 | isTConName n' ctxt = ctyn == n'

1677 | isTConName n' ctxt = ctyn == n'

1666 | otherwise = True

1678 | otherwise = True

1667 -- Variables match anything

1679 -- Variables match anything

1668− matching (V _) _ = True

1680+ matching (V _) _ = True

1669− matching _ (V _) = True

1681+ matching _ (V _) = True

1670 matching _ (P _ n _) = not (isTConName n ctxt)

1682 matching _ (P _ n _) = not (isTConName n ctxt)

1671 matching (P _ n _) _ = not (isTConName n ctxt)

1683 matching (P _ n _) _ = not (isTConName n ctxt)

1672 -- Binders are a plausible match, so keep them

1684 -- Binders are a plausible match, so keep them

src/Idris/Elab/Type.hs+31−14

@@ -52,8 +52,13 @@ import Data.List.Split (splitOn)

53import Util.Pretty(pretty, text)

55−buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

55+buildType :: ElabInfo

56+ -> SyntaxInfo

57+ -> FC

58+ -> FnOpts

59+ -> Name

60+ -> PTerm

56− Idris (Type, Type, PTerm, [(Int, Name)])

61+ -> Idris (Type, Type, PTerm, [(Int, Name)])

57buildType info syn fc opts n ty' = do

62buildType info syn fc opts n ty' = do

58 ctxt <- getContext

63 ctxt <- getContext

59 i <- getIState

64 i <- getIState

@@ -69,13 +74,13 @@ buildType info syn fc opts n ty' = do

70 ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-

75 ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-

71 tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState

76 tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState

72− (errAt "type of " n Nothing

77+ (errAt "type of " n Nothing

73 (erunAux fc (build i info ETyDecl [] n ty)))

78 (erunAux fc (build i info ETyDecl [] n ty)))

75 displayWarnings est

80 displayWarnings est

76 setContext ctxt'

81 setContext ctxt'

77 processTacticDecls info newDecls

82 processTacticDecls info newDecls

78− sendHighlighting highlights

83+ sendHighlighting highlights

79 updateIState $ \i -> i { idris_name = newGName }

84 updateIState $ \i -> i { idris_name = newGName }

81 let tyT = patToImp tyT'

86 let tyT = patToImp tyT'

@@ -108,7 +113,7 @@ buildType info syn fc opts n ty' = do

108

113

109 -- Add the names referenced to the call graph, and check we're not

114 -- Add the names referenced to the call graph, and check we're not

110 -- referring to anything less visible

115 -- referring to anything less visible

111− -- In particular, a public/export type can not refer to anything

116+ -- In particular, a public/export type can not refer to anything

112 -- private, but can refer to any public/export

117 -- private, but can refer to any public/export

113 let refs = freeNames cty

118 let refs = freeNames cty

114 nvis <- getFromHideList n

119 nvis <- getFromHideList n

@@ -136,17 +141,29 @@ buildType info syn fc opts n ty' = do

136 param_pos i ns t = []

141 param_pos i ns t = []

137

142

138-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

143-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

139−elabType :: ElabInfo -> SyntaxInfo

144+elabType :: ElabInfo

145+ -> SyntaxInfo

146+ -> Docstring (Either Err PTerm)

140− -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

147+ -> [(Name, Docstring (Either Err PTerm))]

148+ -> FC

141− -> FC -> FnOpts

149+ -> FnOpts

150+ -> Name

142− -> Name -> FC -- ^ The precise location of the name

151+ -> FC -- ^ The precise location of the name

152+ -> PTerm

143− -> PTerm -> Idris Type

153+ -> Idris Type

144elabType = elabType' False

154elabType = elabType' False

145

155

146−elabType' :: Bool -> -- normalise it

156+elabType' :: Bool -- normalise it

157+ -> ElabInfo

147− ElabInfo -> SyntaxInfo ->

158+ -> SyntaxInfo

159+ -> Docstring (Either Err PTerm)

148− Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

160+ -> [(Name, Docstring (Either Err PTerm))]

161+ -> FC

162+ -> FnOpts

163+ -> Name

164+ -> FC

165+ -> PTerm

149− FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type

166+ -> Idris Type

150elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (params info) ty_in

167elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (params info) ty_in

151 n = liftname info n_in in -}

168 n = liftname info n_in in -}

152 do checkUndefined fc n

169 do checkUndefined fc n

src/Idris/Elab/Utils.hs+8−8

@@ -353,12 +353,14 @@ checkVisibility fc n minAcc acc ref

353 else return ()

354

355

356−-- | Find the type constructor arguments that are parameters, given a list of constructor types.

356+-- | Find the type constructor arguments that are parameters, given a

357+-- list of constructor types.

358+--

357−-- Parameters are names which are unchanged across the structure,

359+-- Parameters are names which are unchanged across the structure,

358−-- which appear exactly once in the return type of a constructor

360+-- which appear exactly once in the return type of a constructor

359−-- First, find all applications of the constructor, then check over

361+-- First, find all applications of the constructor, then check over

360−-- them for repeated arguments

362+-- them for repeated arguments

361−findParams :: Name -- ^ the name of the family that we are finding parameters for

363+findParams :: Name -- ^ the name of the family that we are finding parameters for

362 -> [Type] -- ^ the declared constructor types

364 -> [Type] -- ^ the declared constructor types

363 -> [Int]

365 -> [Int]

364findParams tyn ts =

366findParams tyn ts =

@@ -448,5 +450,3 @@ propagateParams i ps t bound (PRef fc hls n)

448 isImplicit (PImp _ _ _ x _ : is) n | x == n = True

450 isImplicit (PImp _ _ _ x _ : is) n | x == n = True

449 isImplicit (_ : is) n = isImplicit is n

451 isImplicit (_ : is) n = isImplicit is n

450propagateParams i ps t bound x = x

452propagateParams i ps t bound x = x

451−

452−

src/Idris/ElabDecls.hs+3−3

@@ -62,7 +62,7 @@ import Data.List.Split (splitOn)

62import Util.Pretty(pretty, text)

65−-- Top level elaborator info, supporting recursive elaboration

65+-- | Top level elaborator info, supporting recursive elaboration

66recinfo :: ElabInfo

67recinfo = EInfo [] emptyContext id Nothing Nothing id elabDecl'

@@ -111,7 +111,7 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

111 elabBelieveMe

112 = do let prim__believe_me = sUN "prim__believe_me"

113 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

114− -- The point is that it is believed to be total, even

114+ -- The point is that it is believed to be total, even

115 -- though it clearly isn't :)

116 setTotality prim__believe_me (Total [])

117 i <- getIState

@@ -210,7 +210,7 @@ elabDecl' what info (PMutual f ps)

210

211 getDataDecls (PNamespace _ _ ds : decls)

212 = getDataDecls ds ++ getDataDecls decls

213− getDataDecls (d : decls)

213+ getDataDecls (d : decls)

214 | isDataDecl d = d : getDataDecls decls

215 | otherwise = getDataDecls decls

216 getDataDecls [] = []

src/Idris/Erasure.hs+16−15

@@ -32,7 +32,8 @@ import Data.IntMap (IntMap)

32import Data.Text (pack)

33import qualified Data.Text as T

35−-- UseMap maps names to the set of used (reachable) argument positions.

35+-- | UseMap maps names to the set of used (reachable) argument

36+-- positions.

36type UseMap = Map Name (IntMap (Set Reason))

37type UseMap = Map Name (IntMap (Set Reason))

38data Arg = Arg Int | Result deriving (Eq, Ord)

39data Arg = Arg Int | Result deriving (Eq, Ord)

@@ -45,26 +46,26 @@ type Node = (Name, Arg)

45type Deps = Map Cond DepSet

46type Deps = Map Cond DepSet

46type Reason = (Name, Int) -- function name, argument index

47type Reason = (Name, Int) -- function name, argument index

48−-- Nodes along with sets of reasons for every one.

49+-- | Nodes along with sets of reasons for every one.

49type DepSet = Map Node (Set Reason)

50type DepSet = Map Node (Set Reason)

51−-- "Condition" is the conjunction

52+-- | "Condition" is the conjunction of elementary assumptions along

52−-- of elementary assumptions along the path from the root.

53+-- the path from the root. Elementary assumption (f, i) means that

53−-- Elementary assumption (f, i) means that "function f uses the argument i".

54+-- "function f uses the argument i".

54type Cond = Set Node

55type Cond = Set Node

56−-- Variables carry certain information with them.

57+-- ^ Variables carry certain information with them.

57data VarInfo = VI

58data VarInfo = VI

58− { viDeps :: DepSet -- dependencies drawn in by the variable

59+ { viDeps :: DepSet -- ^ dependencies drawn in by the variable

59− , viFunArg :: Maybe Int -- which function argument this variable came from (defined only for patvars)

60+ , viFunArg :: Maybe Int -- ^ which function argument this variable came from (defined only for patvars)

60− , viMethod :: Maybe Name -- name of the metamethod represented by the var, if any

61+ , viMethod :: Maybe Name -- ^ name of the metamethod represented by the var, if any

61 }

62 }

62 deriving Show

63 deriving Show

64type Vars = Map Name VarInfo

65type Vars = Map Name VarInfo

66−-- Perform usage analysis, write the relevant information in the internal

67+-- | Perform usage analysis, write the relevant information in the

67−-- structures, returning the list of reachable names.

68+-- internal structures, returning the list of reachable names.

68performUsageAnalysis :: [Name] -> Idris [Name]

69performUsageAnalysis :: [Name] -> Idris [Name]

69performUsageAnalysis startNames = do

70performUsageAnalysis startNames = do

70 ctx <- tt_ctxt <$> getIState

71 ctx <- tt_ctxt <$> getIState

@@ -137,7 +138,7 @@ performUsageAnalysis startNames = do

137 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]

138 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]

138 warn = logErasure 0

139 warn = logErasure 0

139

140

140−-- Find the minimal consistent usage by forward chaining.

141+-- | Find the minimal consistent usage by forward chaining.

141minimalUsage :: Deps -> (Deps, (Set Name, UseMap))

142minimalUsage :: Deps -> (Deps, (Set Name, UseMap))

142minimalUsage = second gather . forwardChain

143minimalUsage = second gather . forwardChain

143 where

144 where

@@ -160,8 +161,8 @@ forwardChain deps

160 remove :: DepSet -> Deps -> Deps

161 remove :: DepSet -> Deps -> Deps

161 remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)

162 remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)

162

163

163−-- Build the dependency graph,

164−-- starting the depth-first search from a list of Names.

164+-- | Build the dependency graph, starting the depth-first search from

165+-- a list of Names.

165buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->

166buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->

166 Context -> [Name] -> Deps

167 Context -> [Name] -> Deps

167buildDepMap ci used externs ctx startNames

168buildDepMap ci used externs ctx startNames

@@ -508,6 +509,6 @@ buildDepMap ci used externs ctx startNames

508 unionMap :: (a -> Deps) -> [a] -> Deps

509 unionMap :: (a -> Deps) -> [a] -> Deps

509 unionMap f = M.unionsWith (M.unionWith S.union) . map f

510 unionMap f = M.unionsWith (M.unionWith S.union) . map f

510

511

511−-- Make a field name out of a data constructor name and field number.

512+-- | Make a field name out of a data constructor name and field number.

512mkFieldName :: Name -> Int -> Name

513mkFieldName :: Name -> Int -> Name

513mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")

514mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")

src/Idris/ErrReverse.hs+6−8

@@ -9,9 +9,8 @@ import Util.Pretty

9import Data.List

10import Debug.Trace

12−-- For display purposes, apply any 'error reversal' transformations so that

12+-- | For display purposes, apply any 'error reversal' transformations

13−-- errors will be more readable

13+-- so that errors will be more readable

14−

15errReverse :: IState -> Term -> Term

14errReverse :: IState -> Term -> Term

16errReverse ist t = rewrite 5 t -- (elideLambdas t)

15errReverse ist t = rewrite 5 t -- (elideLambdas t)

17 where

16 where

@@ -28,7 +27,7 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

28 -- the rule as invalid and return t)

27 -- the rule as invalid and return t)

30 applyNames ns t (Bind n (PVar ty) scl) (Bind n' (PVar ty') scr)

29 applyNames ns t (Bind n (PVar ty) scl) (Bind n' (PVar ty') scr)

31− | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)

30+ | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)

32 (instantiate (P Ref n' ty') scr)

31 (instantiate (P Ref n' ty') scr)

33 | otherwise = t

32 | otherwise = t

34 applyNames ns t l r = matchTerm ns l r t

33 applyNames ns t l r = matchTerm ns l r t

@@ -38,7 +37,7 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

38 matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f

37 matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f

39 a' = matchTerm ns l r a in

38 a' = matchTerm ns l r a in

40 App s f' a'

39 App s f' a'

41− matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b

40+ matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b

42 sc' = matchTerm ns l r sc in

41 sc' = matchTerm ns l r sc in

43 Bind n b' sc'

42 Bind n b' sc'

44 matchTerm ns l r t = t

43 matchTerm ns l r t = t

@@ -48,7 +47,7 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

49 -- If any duplicate mappings, it's a failure

48 -- If any duplicate mappings, it's a failure

50 combine [] = Just []

49 combine [] = Just []

51− combine ((x, t) : xs)

50+ combine ((x, t) : xs)

52 | Just _ <- lookup x xs = Nothing

51 | Just _ <- lookup x xs = Nothing

53 | otherwise = do xs' <- combine xs

52 | otherwise = do xs' <- combine xs

54 Just ((x, t) : xs')

53 Just ((x, t) : xs')

@@ -64,9 +63,8 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

64 -- it as it won't be very enlightening.

63 -- it as it won't be very enlightening.

66 elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

65 elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

67− elideLambdas (Bind n (Lam t) sc)

66+ elideLambdas (Bind n (Lam t) sc)

68 | size sc > 200 = P Ref (sUN "...") Erased

67 | size sc > 200 = P Ref (sUN "...") Erased

69 elideLambdas (Bind n b sc)

68 elideLambdas (Bind n b sc)

70 = Bind n (fmap elideLambdas b) (elideLambdas sc)

69 = Bind n (fmap elideLambdas b) (elideLambdas sc)

71 elideLambdas t = t

70 elideLambdas t = t

72−

src/Idris/Help.hs+16−16

@@ -1,21 +1,21 @@

1module Idris.Help (CmdArg(..), extraHelp) where

3−data CmdArg = ExprArg -- ^ The command takes an expression

3+data CmdArg = ExprArg -- ^ The command takes an expression

4− | NameArg -- ^ The command takes a name

4+ | NameArg -- ^ The command takes a name

5− | FileArg -- ^ The command takes a file

5+ | FileArg -- ^ The command takes a file

6− | ModuleArg -- ^ The command takes a module name

6+ | ModuleArg -- ^ The command takes a module name

7− | PkgArgs -- ^ The command takes a list of package names

7+ | PkgArgs -- ^ The command takes a list of package names

8− | NumberArg -- ^ The command takes a number

8+ | NumberArg -- ^ The command takes a number

9− | NamespaceArg -- ^ The command takes a namespace name

9+ | NamespaceArg -- ^ The command takes a namespace name

10− | OptionArg -- ^ The command takes an option

10+ | OptionArg -- ^ The command takes an option

11− | MetaVarArg -- ^ The command takes a metavariable

11+ | MetaVarArg -- ^ The command takes a metavariable

12− | ColourArg -- ^ The command is the colour-setting command

12+ | ColourArg -- ^ The command is the colour-setting command

13− | NoArg -- ^ No completion (yet!?)

13+ | NoArg -- ^ No completion (yet!?)

14− | SpecialHeaderArg -- ^ do not use

14+ | SpecialHeaderArg -- ^ do not use

15− | ConsoleWidthArg -- ^ The width of the console

15+ | ConsoleWidthArg -- ^ The width of the console

16− | DeclArg -- ^ An Idris declaration, as might be contained in a file

16+ | DeclArg -- ^ An Idris declaration, as might be contained in a file

17− | ManyArgs CmdArg -- ^ Zero or more of one kind of argument

17+ | ManyArgs CmdArg -- ^ Zero or more of one kind of argument

18− | OptionalArg CmdArg -- ^ Zero or one of one kind of argument

18+ | OptionalArg CmdArg -- ^ Zero or one of one kind of argument

19 | SeqArgs CmdArg CmdArg -- ^ One kind of argument followed by another

21instance Show CmdArg where

src/Idris/IBC.hs+59−58

@@ -42,64 +42,64 @@ import Codec.Archive.Zip

42ibcVersion :: Word16

43ibcVersion = 143

45−-- When IBC is being loaded - we'll load different things (and omit different

45+-- | When IBC is being loaded - we'll load different things (and omit

46−-- structures/definitions) depending on which phase we're in

46+-- different structures/definitions) depending on which phase we're in.

47−data IBCPhase = IBC_Building -- ^ when building the module tree

47+data IBCPhase = IBC_Building -- ^ when building the module tree

48− | IBC_REPL Bool -- ^ when loading modules for the REPL

48+ | IBC_REPL Bool -- ^ when loading modules for the REPL Bool = True for top level module

49− -- Bool = True for top level module

50 deriving (Show, Eq)

49 deriving (Show, Eq)

52−data IBCFile = IBCFile { ver :: Word16,

51+data IBCFile = IBCFile {

52+ ver :: Word16

53− sourcefile :: FilePath,

53+ , sourcefile :: FilePath

54− ibc_reachablenames :: ![Name],

54+ , ibc_reachablenames :: ![Name]

55− ibc_imports :: ![(Bool, FilePath)],

55+ , ibc_imports :: ![(Bool, FilePath)]

56− ibc_importdirs :: ![FilePath],

56+ , ibc_importdirs :: ![FilePath]

57− ibc_implicits :: ![(Name, [PArg])],

57+ , ibc_implicits :: ![(Name, [PArg])]

58− ibc_fixes :: ![FixDecl],

58+ , ibc_fixes :: ![FixDecl]

59− ibc_statics :: ![(Name, [Bool])],

59+ , ibc_statics :: ![(Name, [Bool])]

60− ibc_classes :: ![(Name, ClassInfo)],

60+ , ibc_classes :: ![(Name, ClassInfo)]

61− ibc_records :: ![(Name, RecordInfo)],

61+ , ibc_records :: ![(Name, RecordInfo)]

62− ibc_instances :: ![(Bool, Bool, Name, Name)],

62+ , ibc_instances :: ![(Bool, Bool, Name, Name)]

63− ibc_dsls :: ![(Name, DSL)],

63+ , ibc_dsls :: ![(Name, DSL)]

64− ibc_datatypes :: ![(Name, TypeInfo)],

64+ , ibc_datatypes :: ![(Name, TypeInfo)]

65− ibc_optimise :: ![(Name, OptInfo)],

65+ , ibc_optimise :: ![(Name, OptInfo)]

66− ibc_syntax :: ![Syntax],

66+ , ibc_syntax :: ![Syntax]

67− ibc_keywords :: ![String],

67+ , ibc_keywords :: ![String]

68− ibc_objs :: ![(Codegen, FilePath)],

68+ , ibc_objs :: ![(Codegen, FilePath)]

69− ibc_libs :: ![(Codegen, String)],

69+ , ibc_libs :: ![(Codegen, String)]

70− ibc_cgflags :: ![(Codegen, String)],

70+ , ibc_cgflags :: ![(Codegen, String)]

71− ibc_dynamic_libs :: ![String],

71+ , ibc_dynamic_libs :: ![String]

72− ibc_hdrs :: ![(Codegen, String)],

72+ , ibc_hdrs :: ![(Codegen, String)]

73− ibc_totcheckfail :: ![(FC, String)],

73+ , ibc_totcheckfail :: ![(FC, String)]

74− ibc_flags :: ![(Name, [FnOpt])],

74+ , ibc_flags :: ![(Name, [FnOpt])]

75− ibc_fninfo :: ![(Name, FnInfo)],

75+ , ibc_fninfo :: ![(Name, FnInfo)]

76− ibc_cg :: ![(Name, CGInfo)],

76+ , ibc_cg :: ![(Name, CGInfo)]

77− ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

77+ , ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))]

78− ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],

78+ , ibc_moduledocs :: ![(Name, Docstring D.DocTerm)]

79− ibc_transforms :: ![(Name, (Term, Term))],

79+ , ibc_transforms :: ![(Name, (Term, Term))]

80− ibc_errRev :: ![(Term, Term)],

80+ , ibc_errRev :: ![(Term, Term)]

81− ibc_coercions :: ![Name],

81+ , ibc_coercions :: ![Name]

82− ibc_lineapps :: ![(FilePath, Int, PTerm)],

82+ , ibc_lineapps :: ![(FilePath, Int, PTerm)]

83− ibc_namehints :: ![(Name, Name)],

83+ , ibc_namehints :: ![(Name, Name)]

84− ibc_metainformation :: ![(Name, MetaInformation)],

84+ , ibc_metainformation :: ![(Name, MetaInformation)]

85− ibc_errorhandlers :: ![Name],

85+ , ibc_errorhandlers :: ![Name]

86− ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler

86+ , ibc_function_errorhandlers :: ![(Name, Name, Name)] -- fn, arg, handler

87− ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool, Bool))],

87+ , ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool, Bool))]

88− ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))],

88+ , ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))]

89− ibc_postulates :: ![Name],

89+ , ibc_postulates :: ![Name]

90− ibc_externs :: ![(Name, Int)],

90+ , ibc_externs :: ![(Name, Int)]

91− ibc_parsedSpan :: !(Maybe FC),

91+ , ibc_parsedSpan :: !(Maybe FC)

92− ibc_usage :: ![(Name, Int)],

92+ , ibc_usage :: ![(Name, Int)]

93− ibc_exports :: ![Name],

93+ , ibc_exports :: ![Name]

94− ibc_autohints :: ![(Name, Name)],

94+ , ibc_autohints :: ![(Name, Name)]

95− ibc_deprecated :: ![(Name, String)],

95+ , ibc_deprecated :: ![(Name, String)]

96− ibc_defs :: ![(Name, Def)],

96+ , ibc_defs :: ![(Name, Def)]

97− ibc_total :: ![(Name, Totality)],

97+ , ibc_total :: ![(Name, Totality)]

98− ibc_injective :: ![(Name, Injectivity)],

98+ , ibc_injective :: ![(Name, Injectivity)]

99− ibc_access :: ![(Name, Accessibility)],

99+ , ibc_access :: ![(Name, Accessibility)]

100− ibc_fragile :: ![(Name, String)]

100+ , ibc_fragile :: ![(Name, String)]

101− }

101+ }

102− deriving Show

102+ deriving Show

103{-!

104deriving instance Binary IBCFile

105!-}

@@ -221,8 +221,9 @@ writeIBC src f

221 (\c -> do logIBC 1 $ "Failed " ++ pshow i c)

222 return ()

223

224−-- Write a package index containing all the imports in the current IState

224+-- | Write a package index containing all the imports in the current

225−-- Used for ':search' of an entire package, to ensure everything is loaded.

225+-- IState Used for ':search' of an entire package, to ensure

226+-- everything is loaded.

226writePkgIndex :: FilePath -> Idris ()

227writePkgIndex :: FilePath -> Idris ()

227writePkgIndex f

228writePkgIndex f

228 = do i <- getIState

229 = do i <- getIState

src/Idris/Imports.hs+2−2

@@ -103,11 +103,11 @@ installedPackages = do

103 goodDir idir d = any (".ibc" `isSuffixOf`) <$> allFilesInDir idir d

104

105

106−-- Case sensitive file existence check for Mac OS X.

106+-- | Case sensitive file existence check for Mac OS X.

107doesFileExist' :: FilePath -> IO Bool

108doesFileExist' = caseSensitive doesFileExist

109

110−-- Case sensitive directory existence check for Mac OS X.

110+-- | Case sensitive directory existence check for Mac OS X.

111doesDirectoryExist' :: FilePath -> IO Bool

112doesDirectoryExist' = caseSensitive doesDirectoryExist

113

src/Idris/Inliner.hs+2−4

@@ -8,8 +8,8 @@ import Idris.AbsSyntax

8inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]

9inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds

11−-- Inlining is either top level (i.e. not in a function arg) or argument level

11+-- | Inlining is either top level (i.e. not in a function arg) or argument level

12−

12+--

13-- For each application in a term:

14-- * Check if the function is inlinable

15-- (Dictionaries are inlinable in an argument, not otherwise)

@@ -17,7 +17,6 @@ inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds

17-- + If successful, then continue on the result (top level)

18-- + If not, reduce the arguments (argument level) and try again

19-- - If not, inline all the arguments (top level)

20−

21inlineTerm :: IState -> Term -> Term

20inlineTerm :: IState -> Term -> Term

22inlineTerm ist tm = inl tm where

21inlineTerm ist tm = inl tm where

23 inl orig@(P _ n _) = inlApp n [] orig

22 inl orig@(P _ n _) = inlApp n [] orig

@@ -28,4 +27,3 @@ inlineTerm ist tm = inl tm where

28 inl tm = tm

27 inl tm = tm

30 inlApp fn args orig = orig

29 inlApp fn args orig = orig

31−

src/Idris/Parser.hs+42−43

@@ -89,7 +89,7 @@ import System.IO

90{- * Main grammar -}

92−{- | Parses module definition

92+{-| Parses module definition

94@

95 ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;

@@ -122,7 +122,7 @@ data ImportInfo = ImportInfo { import_reexport :: Bool

122 , import_modname_location :: FC

123 }

124

125−{- | Parses an import statement

125+{-| Parses an import statement

126

127@

128 Import ::= 'import' Identifier_t ';'?;

@@ -144,7 +144,7 @@ import_ = do fc <- getFC

144 where ns = Spl.splitOn "."

145 toPath = foldl1' (</>) . ns

146

147−{- | Parses program source

147+{-| Parses program source

148

149@

150 Prog ::= Decl* EOF;

@@ -238,7 +238,7 @@ internalDecl syn

238 continue False (PClauses _ _ _ _) = True

239 continue c _ = c

240

241−{- | Parses a top-level declaration with possible syntax sugar

241+{-| Parses a top-level declaration with possible syntax sugar

242

243@

244Decl' ::=

@@ -387,7 +387,7 @@ declExtension syn ns rules =

387 highlightP fc AnnKeyword

388 return Nothing

389

390−{- | Parses a syntax extension declaration (and adds the rule to parser state)

390+{-| Parses a syntax extension declaration (and adds the rule to parser state)

391

392@

393 SyntaxDecl ::= SyntaxRule;

@@ -418,7 +418,7 @@ addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs,

418 ns = syntax_keywords i

419 ks = map show (syntaxNames s)

420

421−{- | Parses a syntax extension declaration

421+{-| Parses a syntax extension declaration

422

423@

424SyntaxRuleOpts ::= 'term' | 'pattern';

@@ -545,7 +545,7 @@ syntaxRule syn

545 put ist { idris_name = idx + 1 }

546 return $ sMN idx (show n)

547

548−{- | Parses a syntax symbol (either binding variable, keyword or expression)

548+{-| Parses a syntax symbol (either binding variable, keyword or expression)

549

550@

551SyntaxSym ::= '[' Name_t ']'

@@ -566,7 +566,7 @@ syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'

566 return (Symbol sym)

567 <?> "syntax symbol"

568

569−{- | Parses a function declaration with possible syntax sugar

569+{-| Parses a function declaration with possible syntax sugar

570

571@

572 FunDecl ::= FunDecl';

@@ -715,7 +715,7 @@ fnOpt = do reservedHL "total"; return TotalFn

715 return (Just (fromInteger reds)))

716 return (n, t)

717

718−{- | Parses a postulate

718+{-| Parses a postulate

719

720@

721Postulate ::=

@@ -742,7 +742,8 @@ postulate syn = do (doc, ext)

742 <?> "postulate"

743 where ppostDecl = do fc <- reservedHL "postulate"; return False

744 <|> do lchar '%'; reserved "extern"; return True

745+

745−{- | Parses a using declaration

746+{-| Parses a using declaration

746

747

747@

748@

748Using ::=

749Using ::=

@@ -761,14 +762,14 @@ using_ syn =

761 return (concat ds)

762 return (concat ds)

762 <?> "using declaration"

763 <?> "using declaration"

763

764

764−{- | Parses a parameters declaration

765+{-| Parses a parameters declaration

765

766

766@

767@

767Params ::=

768Params ::=

768 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock

769 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock

769 ;

770 ;

770@

771@

771− -}

772+-}

772params :: SyntaxInfo -> IdrisParser [PDecl]

773params :: SyntaxInfo -> IdrisParser [PDecl]

773params syn =

774params syn =

774 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

775 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

@@ -781,10 +782,7 @@ params syn =

781 return [PParams fc ns' (concat ds)]

782 return [PParams fc ns' (concat ds)]

782 <?> "parameters declaration"

783 <?> "parameters declaration"

783

784

784−{- | Parses an open block

785+-- | Parses an open block

785−

786−-}

787−

788openInterface :: SyntaxInfo -> IdrisParser [PDecl]

786openInterface :: SyntaxInfo -> IdrisParser [PDecl]

789openInterface syn =

787openInterface syn =

790 do reservedHL "using"

788 do reservedHL "using"

@@ -799,9 +797,10 @@ openInterface syn =

799 <?> "open interface declaration"

797 <?> "open interface declaration"

800

798

801

799

800+

802

801

803

802

804−{- | Parses a mutual declaration (for mutually recursive functions)

803+{-| Parses a mutual declaration (for mutually recursive functions)

805

804

806@

805@

807Mutual ::=

806Mutual ::=

@@ -838,7 +837,7 @@ namespace syn =

838 return [PNamespace n nfc (concat ds)]

837 return [PNamespace n nfc (concat ds)]

839 <?> "namespace declaration"

838 <?> "namespace declaration"

840

839

841−{- | Parses a methods block (for instances)

840+{-| Parses a methods block (for instances)

842

841

843@

842@

844 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

843 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

@@ -852,7 +851,7 @@ instanceBlock syn = do reservedHL "where"

852 return (concat ds)

851 return (concat ds)

853 <?> "implementation block"

852 <?> "implementation block"

854

853

855−{- | Parses a methods and instances block (for type classes)

854+{-| Parses a methods and instances block (for type classes)

856

855

857@

856@

858MethodOrInstance ::=

857MethodOrInstance ::=

@@ -941,7 +940,7 @@ class_ syn = do (doc, argDocs, acc)

941 fc <- getFC

940 fc <- getFC

942 return (i, ifc, PType fc)

941 return (i, ifc, PType fc)

943

942

944−{- | Parses a type class instance declaration

943+{-| Parses a type class instance declaration

945

944

946@

945@

947 Instance ::=

946 Instance ::=

@@ -1003,7 +1002,7 @@ docstring syn = do (doc, argDocs) <- option noDocs docComment

1003 return (doc', argDocs')

1002 return (doc', argDocs')

1004

1003

1005

1004

1006−{- | Parses a using declaration list

1005+{-| Parses a using declaration list

1007

1006

1008@

1007@

1009UsingDeclList ::=

1008UsingDeclList ::=

@@ -1035,7 +1034,7 @@ usingDeclList syn

1035 return (map (\x -> UImplicit x t) ns)

1034 return (map (\x -> UImplicit x t) ns)

1036 <?> "using declaration list"

1035 <?> "using declaration list"

1037

1036

1038−{- |Parses a using declaration

1037+{-| Parses a using declaration

1039

1038

1040@

1039@

1041UsingDecl ::=

1040UsingDecl ::=

@@ -1054,7 +1053,7 @@ usingDecl syn = try (do x <- fst <$> fnName

1054 return (UConstraint c xs)

1053 return (UConstraint c xs)

1055 <?> "using declaration"

1054 <?> "using declaration"

1056

1055

1057−{- | Parse a clause with patterns

1056+{-| Parse a clause with patterns

1058

1057

1059@

1058@

1060Pattern ::= Clause;

1059Pattern ::= Clause;

@@ -1066,7 +1065,7 @@ pattern syn = do fc <- getFC

1066 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later

1065 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later

1067 <?> "pattern"

1066 <?> "pattern"

1068

1067

1069−{- | Parse a constant applicative form declaration

1068+{-| Parse a constant applicative form declaration

1070

1069

1071@

1070@

1072CAF ::= 'let' FnName '=' Expr Terminator;

1071CAF ::= 'let' FnName '=' Expr Terminator;

@@ -1083,7 +1082,7 @@ caf syn = do reservedHL "let"

1083 return (PCAF fc n t)

1082 return (PCAF fc n t)

1084 <?> "constant applicative form declaration"

1083 <?> "constant applicative form declaration"

1085

1084

1086−{- | Parse an argument expression

1085+{-| Parse an argument expression

1087

1086

1088@

1087@

1089ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

1088ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

@@ -1094,7 +1093,7 @@ argExpr syn = let syn' = syn { inPattern = True } in

1094 try (hsimpleExpr syn') <|> simpleExternalExpr syn'

1093 try (hsimpleExpr syn') <|> simpleExternalExpr syn'

1095 <?> "argument expression"

1094 <?> "argument expression"

1096

1095

1097−{- | Parse a right hand side of a function

1096+{-| Parse a right hand side of a function

1098

1097

1099@

1098@

1100RHS ::= '=' Expr

1099RHS ::= '=' Expr

@@ -1130,7 +1129,7 @@ rhs syn n = do lchar '='; expr syn

1130 where addLetC (l, r) = (l, addLet fc nm r)

1129 where addLetC (l, r) = (l, addLet fc nm r)

1131 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))

1130 addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))

1132

1131

1133−{- |Parses a function clause

1132+{-|Parses a function clause

1134

1133

1135@

1134@

1136RHSOrWithBlock ::= RHS WhereOrTerminator

1135RHSOrWithBlock ::= RHS WhereOrTerminator

@@ -1296,7 +1295,7 @@ wExpr syn = do lchar '|'

1296 expr' (syn { inPattern = True })

1295 expr' (syn { inPattern = True })

1297 <?> "with pattern"

1296 <?> "with pattern"

1298

1297

1299−{- | Parses a where block

1298+{-| Parses a where block

1300

1299

1301@

1300@

1302WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

1301WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

@@ -1310,7 +1309,7 @@ whereBlock n syn

1310 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1309 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1311 <?> "where block"

1310 <?> "where block"

1312

1311

1313−{- |Parses a code generation target language name

1312+{-|Parses a code generation target language name

1314

1313

1315@

1314@

1316Codegen ::= 'C'

1315Codegen ::= 'C'

@@ -1328,7 +1327,7 @@ codegen_ = do n <- fst <$> identifier

1328 <|> do reserved "Bytecode"; return Bytecode

1327 <|> do reserved "Bytecode"; return Bytecode

1329 <?> "code generation language"

1328 <?> "code generation language"

1330

1329

1331−{- |Parses a compiler directive

1330+{-|Parses a compiler directive

1332@

1331@

1333StringList ::=

1332StringList ::=

1334 String

1333 String

@@ -1433,7 +1432,7 @@ pLangExt :: IdrisParser LanguageExt

1433pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1432pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1434 <|> (reserved "ErrorReflection" >> return ErrorReflection)

1433 <|> (reserved "ErrorReflection" >> return ErrorReflection)

1435

1434

1436−{- | Parses a totality

1435+{-| Parses a totality

1437

1436

1438@

1437@

1439Totality ::= 'partial' | 'total' | 'covering'

1438Totality ::= 'partial' | 'total' | 'covering'

@@ -1446,7 +1445,7 @@ totality

1446 <|> do reservedHL "partial"; return DefaultCheckingPartial

1445 <|> do reservedHL "partial"; return DefaultCheckingPartial

1447 <|> do reservedHL "covering"; return DefaultCheckingCovering

1446 <|> do reservedHL "covering"; return DefaultCheckingCovering

1448

1447

1449−{- | Parses a type provider

1448+{-| Parses a type provider

1450

1449

1451@

1450@

1452Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1451Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

@@ -1476,7 +1475,7 @@ provider syn = do doc <- try (do (doc, _) <- docstring syn

1476 e <- expr syn <?> "provider expression"

1475 e <- expr syn <?> "provider expression"

1477 return [PProvider doc syn fc nfc (ProvPostulate e) n]

1476 return [PProvider doc syn fc nfc (ProvPostulate e) n]

1478

1477

1479−{- | Parses a transform

1478+{-| Parses a transform

1480

1479

1481@

1480@

1482Transform ::= '%' 'transform' Expr '==>' Expr

1481Transform ::= '%' 'transform' Expr '==>' Expr

@@ -1495,7 +1494,7 @@ transform syn = do try (lchar '%' *> reserved "transform")

1495 return [PTransform fc False l r]

1494 return [PTransform fc False l r]

1496 <?> "transform"

1495 <?> "transform"

1497

1496

1498−{- | Parses a top-level reflected elaborator script

1497+{-| Parses a top-level reflected elaborator script

1499

1498

1500@

1499@

1501RunElabDecl ::= '%' 'runElab' Expr

1500RunElabDecl ::= '%' 'runElab' Expr

@@ -1513,19 +1512,19 @@ runElabDecl syn =

1513 <?> "top-level elaborator script"

1512 <?> "top-level elaborator script"

1514

1513

1515{- * Loading and parsing -}

1514{- * Loading and parsing -}

1516−{- | Parses an expression from input -}

1515+{-| Parses an expression from input -}

1517parseExpr :: IState -> String -> Result PTerm

1516parseExpr :: IState -> String -> Result PTerm

1518parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1517parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1519

1518

1520−{- | Parses a constant form input -}

1519+{-| Parses a constant form input -}

1521parseConst :: IState -> String -> Result Const

1520parseConst :: IState -> String -> Result Const

1522parseConst st = runparser (fmap fst constant) st "(input)"

1521parseConst st = runparser (fmap fst constant) st "(input)"

1523

1522

1524−{- | Parses a tactic from input -}

1523+{-| Parses a tactic from input -}

1525parseTactic :: IState -> String -> Result PTactic

1524parseTactic :: IState -> String -> Result PTactic

1526parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1525parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1527

1526

1528−{- | Parses a do-step from input (used in the elab shell) -}

1527+{-| Parses a do-step from input (used in the elab shell) -}

1529parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

1528parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

1530parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"

1529parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"

1531 where elabShellCmd = char ':' >>

1530 where elabShellCmd = char ':' >>

@@ -1639,7 +1638,7 @@ parseProg syn fname input mrk

1639 i' <- get

1638 i' <- get

1640 return (ds, i')

1639 return (ds, i')

1641

1640

1642−{- | Load idris module and show error if something wrong happens -}

1641+{-| Load idris module and show error if something wrong happens -}

1643loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

1642loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

1644loadModule f phase

1643loadModule f phase

1645 = idrisCatch (loadModule' f phase)

1644 = idrisCatch (loadModule' f phase)

@@ -1648,7 +1647,7 @@ loadModule f phase

1648 iWarn (getErrSpan e) $ pprintErr ist e

1647 iWarn (getErrSpan e) $ pprintErr ist e

1649 return Nothing)

1648 return Nothing)

1650

1649

1651−{- | Load idris module -}

1650+{-| Load idris module -}

1652loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)

1651loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)

1653loadModule' f phase

1652loadModule' f phase

1654 = do i <- getIState

1653 = do i <- getIState

@@ -1671,7 +1670,7 @@ loadModule' f phase

1671 LIDR sfn -> loadSource True sfn Nothing)

1670 LIDR sfn -> loadSource True sfn Nothing)

1672 return $ Just file

1671 return $ Just file

1673

1672

1674−{- | Load idris code from file -}

1673+{-| Load idris code from file -}

1675loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1674loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1676loadFromIFile reexp phase i@(IBC fn src) maxline

1675loadFromIFile reexp phase i@(IBC fn src) maxline

1677 = do logParser 1 $ "Skipping " ++ getSrcFile i

1676 = do logParser 1 $ "Skipping " ++ getSrcFile i

@@ -1695,7 +1694,7 @@ loadSource' lidr r maxline

1695 At f e' -> iWarn f (pprintErr ist e')

1694 At f e' -> iWarn f (pprintErr ist e')

1696 _ -> iWarn (getErrSpan e) (pprintErr ist e))

1695 _ -> iWarn (getErrSpan e) (pprintErr ist e))

1697

1696

1698−{- | Load Idris source code-}

1697+{-| Load Idris source code-}

1699loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

1698loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

1700loadSource lidr f toline

1699loadSource lidr f toline

1701 = do logParser 1 ("Reading " ++ f)

1700 = do logParser 1 ("Reading " ++ f)

@@ -1878,7 +1877,7 @@ loadSource lidr f toline

1878 docName = NS modDocName (map T.pack (reverse mname))

1877 docName = NS modDocName (map T.pack (reverse mname))

1879 parsedDocs ist = annotCode (tryFullExpr syn ist) docs

1878 parsedDocs ist = annotCode (tryFullExpr syn ist) docs

1880

1879

1881−{- | Adds names to hide list -}

1880+{-| Adds names to hide list -}

1882addHides :: Ctxt Accessibility -> Idris ()

1881addHides :: Ctxt Accessibility -> Idris ()

1883addHides xs = do i <- getIState

1882addHides xs = do i <- getIState

1884 let defh = default_access i

1883 let defh = default_access i

src/Idris/Parser/Data.hs+1−1

@@ -37,7 +37,7 @@ import qualified Data.ByteString.UTF8 as UTF8

38import Debug.Trace

40−{- |Parses a record type declaration

40+{- | Parses a record type declaration

41Record ::=

42 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

43-}

src/Idris/PartialEval.hs+51−46

@@ -27,11 +27,12 @@ data PEArgType = ImplicitS -- ^ Implicit static argument

27-- | A partially evaluated function. pe_app captures the lhs of the

28-- new definition, pe_def captures the rhs, and pe_clauses is the

29-- specialised implementation.

30+--

30−-- pe_simple is set if the result is always reducible, because in such a

31+-- pe_simple is set if the result is always reducible, because in such

31−-- case we'll also need to reduce the static argument

32+-- a case we'll also need to reduce the static argument

32data PEDecl = PEDecl { pe_app :: PTerm, -- new application

33data PEDecl = PEDecl { pe_app :: PTerm, -- new application

33 pe_def :: PTerm, -- old application

34 pe_def :: PTerm, -- old application

34− pe_clauses :: [(PTerm, PTerm)], -- clauses of new application

35+ pe_clauses :: [(PTerm, PTerm)], -- clauses of new application

35 pe_simple :: Bool -- if just one reducible clause

36 pe_simple :: Bool -- if just one reducible clause

36 }

37 }

@@ -42,14 +43,14 @@ data PEDecl = PEDecl { pe_app :: PTerm, -- new application

42-- must have reduced at least once.

43-- must have reduced at least once.

43-- If we don't do this, we might end up making an infinite function after

44-- If we don't do this, we might end up making an infinite function after

44-- applying the transformation.

45-- applying the transformation.

45−partial_eval :: Context ->

46+partial_eval :: Context

46− [(Name, Maybe Int)] ->

47+ -> [(Name, Maybe Int)]

47− [Either Term (Term, Term)] ->

48+ -> [Either Term (Term, Term)]

48− Maybe [Either Term (Term, Term)]

49+ -> Maybe [Either Term (Term, Term)]

49partial_eval ctxt ns_in tms = mapM peClause tms where

50partial_eval ctxt ns_in tms = mapM peClause tms where

50 ns = squash ns_in

51 ns = squash ns_in

51− squash ((n, Just x) : ns)

52+ squash ((n, Just x) : ns)

52− | Just (Just y) <- lookup n ns

53+ | Just (Just y) <- lookup n ns

53 = squash ((n, Just (x + y)) : drop n ns)

54 = squash ((n, Just (x + y)) : drop n ns)

54 | otherwise = (n, Just x) : squash ns

55 | otherwise = (n, Just x) : squash ns

55 squash (n : ns) = n : squash ns

56 squash (n : ns) = n : squash ns

@@ -58,7 +59,7 @@ partial_eval ctxt ns_in tms = mapM peClause tms where

58 drop n ((m, _) : ns) | n == m = ns

59 drop n ((m, _) : ns) | n == m = ns

59 drop n (x : ns) = x : drop n ns

60 drop n (x : ns) = x : drop n ns

60 drop n [] = []

61 drop n [] = []

61−

62+

62 -- If the term is not a clause, it is simply kept as is

63 -- If the term is not a clause, it is simply kept as is

63 peClause (Left t) = Just $ Left t

64 peClause (Left t) = Just $ Left t

64 -- If the term is a clause, specialise the right hand side

65 -- If the term is a clause, specialise the right hand side

@@ -68,7 +69,7 @@ partial_eval ctxt ns_in tms = mapM peClause tms where

68 return (Right (lhs, rhs'))

69 return (Right (lhs, rhs'))

70 -- TMP HACK until I do PE by WHNF rather than using main evaluator

71 -- TMP HACK until I do PE by WHNF rather than using main evaluator

71− toLimit (n, Nothing) | isTCDict n ctxt = (n, 2)

72+ toLimit (n, Nothing) | isTCDict n ctxt = (n, 2)

72 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

73 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

73 toLimit (n, Just l) = (n, l)

74 toLimit (n, Just l) = (n, l)

@@ -103,7 +104,7 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

103 unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi i t k) sc)

104 unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi i t k) sc)

104 = do amap <- get

105 = do amap <- get

105 case lookup imp amap of

106 case lookup imp amap of

106− Just n' ->

107+ Just n' ->

107 do put (amap ++ [((UnifiedD, Erased), n)])

108 do put (amap ++ [((UnifiedD, Erased), n)])

108 sc' <- unifyEq xs (subst n (P Bound n' Erased) sc)

109 sc' <- unifyEq xs (subst n (P Bound n' Erased) sc)

109 return (Bind n (Pi i t k) sc') -- erase later

110 return (Bind n (Pi i t k) sc') -- erase later

@@ -119,12 +120,12 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

119 put (args ++ (zip xs (repeat (sUN "_"))))

120 put (args ++ (zip xs (repeat (sUN "_"))))

120 return t

121 return t

121

122

122−-- | Creates an Idris type declaration given current state and a

123+-- | Creates an Idris type declaration given current state and a

123-- specialised TT function application type.

124-- specialised TT function application type.

124-- Can be used in combination with the output of 'specType'.

125-- Can be used in combination with the output of 'specType'.

125--

126--

126-- This should: specialise any static argument position, then generalise

127-- This should: specialise any static argument position, then generalise

127−-- over any function applications in the result.

128+-- over any function applications in the result.

128mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

129mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

129mkPE_TyDecl ist args ty = mkty args ty

130mkPE_TyDecl ist args ty = mkty args ty

130 where

131 where

@@ -132,7 +133,7 @@ mkPE_TyDecl ist args ty = mkty args ty

132 = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

133 = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

133 mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

134 mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

134 | concreteClass ist t = mkty xs sc

135 | concreteClass ist t = mkty xs sc

135− | classConstraint ist t

136+ | classConstraint ist t

136 = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

137 = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

137 | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

138 | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

138

139

@@ -141,7 +142,7 @@ mkPE_TyDecl ist args ty = mkty args ty

141 mkty [] t = delab ist t

142 mkty [] t = delab ist t

142

143

143 generaliseIn tm = evalState (gen tm) 0

144 generaliseIn tm = evalState (gen tm) 0

144−

145+

145 gen tm | (P _ fn _, args) <- unApply tm,

146 gen tm | (P _ fn _, args) <- unApply tm,

146 isFnName fn (tt_ctxt ist)

147 isFnName fn (tt_ctxt ist)

147 = do nm <- get

148 = do nm <- get

@@ -166,26 +167,26 @@ concreteClass ist v

166 | (P _ c _, args) <- unApply v = all concrete args

167 | (P _ c _, args) <- unApply v = all concrete args

167 | otherwise = False

168 | otherwise = False

168 where concrete (Constant _) = True

169 where concrete (Constant _) = True

169− concrete tm | (P _ n _, args) <- unApply tm

170+ concrete tm | (P _ n _, args) <- unApply tm

170 = case lookupTy n (tt_ctxt ist) of

171 = case lookupTy n (tt_ctxt ist) of

171 [_] -> all concrete args

172 [_] -> all concrete args

172 _ -> False

173 _ -> False

173 | otherwise = False

174 | otherwise = False

174

175

175−mkNewPats :: IState ->

176+mkNewPats :: IState

176− [(Term, Term)] -> -- definition to specialise

177+ -> [(Term, Term)] -- ^ definition to specialise

177− [(PEArgType, Term)] -> -- arguments to specialise with

178+ -> [(PEArgType, Term)] -- ^ arguments to specialise with

178− Name -> -- New name

179+ -> Name -- ^ New name

179− Name -> -- Specialised function name

180+ -> Name -- ^ Specialised function name

180− PTerm -> -- Default lhs

181+ -> PTerm -- ^ Default lhs

181− PTerm -> -- Default rhs

182+ -> PTerm -- ^ Default rhs

182− PEDecl

183+ -> PEDecl

183-- If all of the dynamic positions on the lhs are variables (rather than

184-- If all of the dynamic positions on the lhs are variables (rather than

184-- patterns or constants) then we can just make a simple definition

185-- patterns or constants) then we can just make a simple definition

185-- directly applying the specialised function, since we know the

186-- directly applying the specialised function, since we know the

186-- definition isn't going to block on any of the dynamic arguments

187-- definition isn't going to block on any of the dynamic arguments

187-- in this case

188-- in this case

188−mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

189+mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

189 = PEDecl lhs rhs [(lhs, rhs)] True

190 = PEDecl lhs rhs [(lhs, rhs)] True

190 where dynVar ap = case unApply ap of

191 where dynVar ap = case unApply ap of

191 (_, args) -> dynArgs ns args

192 (_, args) -> dynArgs ns args

@@ -197,32 +198,32 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

197 -- do some more work

198 -- do some more work

198 dynArgs (_ : ns) (V _ : as) = dynArgs ns as

199 dynArgs (_ : ns) (V _ : as) = dynArgs ns as

199 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

200 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

200− dynArgs _ _ = False -- and now we'll get stuck

201+ dynArgs _ _ = False -- and now we'll get stuck

201

202

202mkNewPats ist d ns newname sname lhs rhs =

203mkNewPats ist d ns newname sname lhs rhs =

203 PEDecl lhs rhs (map mkClause d) False

204 PEDecl lhs rhs (map mkClause d) False

204− where

205+ where

205 mkClause :: (Term, Term) -> (PTerm, PTerm)

206 mkClause :: (Term, Term) -> (PTerm, PTerm)

206 mkClause (oldlhs, oldrhs)

207 mkClause (oldlhs, oldrhs)

207− = let (_, as) = unApply oldlhs

208+ = let (_, as) = unApply oldlhs

208 lhsargs = mkLHSargs [] ns as

209 lhsargs = mkLHSargs [] ns as

209 lhs = PApp emptyFC (PRef emptyFC [] newname) lhsargs

210 lhs = PApp emptyFC (PRef emptyFC [] newname) lhsargs

210− rhs = PApp emptyFC (PRef emptyFC [] sname)

211+ rhs = PApp emptyFC (PRef emptyFC [] sname)

211 (mkRHSargs ns lhsargs) in

212 (mkRHSargs ns lhsargs) in

212 (lhs, rhs)

213 (lhs, rhs)

213

214

214 mkLHSargs _ [] _ = []

215 mkLHSargs _ [] _ = []

215 -- dynamics don't appear if they're implicit

216 -- dynamics don't appear if they're implicit

216− mkLHSargs sub ((ExplicitD, t) : ns) (a : as)

217+ mkLHSargs sub ((ExplicitD, t) : ns) (a : as)

217 = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as

218 = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as

218− mkLHSargs sub ((ImplicitD, _) : ns) (a : as)

219+ mkLHSargs sub ((ImplicitD, _) : ns) (a : as)

219 = mkLHSargs sub ns as

220 = mkLHSargs sub ns as

220− mkLHSargs sub ((UnifiedD, _) : ns) (a : as)

221+ mkLHSargs sub ((UnifiedD, _) : ns) (a : as)

221 = mkLHSargs sub ns as

222 = mkLHSargs sub ns as

222 -- statics get dropped in any case

223 -- statics get dropped in any case

223− mkLHSargs sub ((ImplicitS, t) : ns) (a : as)

224+ mkLHSargs sub ((ImplicitS, t) : ns) (a : as)

224 = mkLHSargs (extend a t sub) ns as

225 = mkLHSargs (extend a t sub) ns as

225− mkLHSargs sub ((ExplicitS, t) : ns) (a : as)

226+ mkLHSargs sub ((ExplicitS, t) : ns) (a : as)

226 = mkLHSargs (extend a t sub) ns as

227 = mkLHSargs (extend a t sub) ns as

227 mkLHSargs sub _ [] = [] -- no more LHS

228 mkLHSargs sub _ [] = [] -- no more LHS

228

229

@@ -237,20 +238,23 @@ mkNewPats ist d ns newname sname lhs rhs =

237 mkSubst :: (Term, Term) -> Maybe (Name, Term)

238 mkSubst :: (Term, Term) -> Maybe (Name, Term)

238 mkSubst (P _ n _, t) = Just (n, t)

239 mkSubst (P _ n _, t) = Just (n, t)

239 mkSubst _ = Nothing

240 mkSubst _ = Nothing

240−

241+

241-- | Creates a new declaration for a specialised function application.

242-- | Creates a new declaration for a specialised function application.

242-- Simple version at the moment: just create a version which is a direct

243-- Simple version at the moment: just create a version which is a direct

243-- application of the function to be specialised.

244-- application of the function to be specialised.

244-- More complex version to do: specialise the definition clause by clause

245-- More complex version to do: specialise the definition clause by clause

245−mkPE_TermDecl :: IState -> Name -> Name ->

246+mkPE_TermDecl :: IState

247+ -> Name

248+ -> Name

246− [(PEArgType, Term)] -> PEDecl

249+ -> [(PEArgType, Term)]

250+ -> PEDecl

247−mkPE_TermDecl ist newname sname ns

251+mkPE_TermDecl ist newname sname ns

248− = let lhs = PApp emptyFC (PRef emptyFC [] newname) (map pexp (mkp ns))

252+ = let lhs = PApp emptyFC (PRef emptyFC [] newname) (map pexp (mkp ns))

249− rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

253+ rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

250 patdef = lookupCtxtExact sname (idris_patdefs ist)

254 patdef = lookupCtxtExact sname (idris_patdefs ist)

251 newpats = case patdef of

255 newpats = case patdef of

252 Nothing -> PEDecl lhs rhs [(lhs, rhs)] True

256 Nothing -> PEDecl lhs rhs [(lhs, rhs)] True

253− Just d -> mkNewPats ist (getPats d) ns

257+ Just d -> mkNewPats ist (getPats d) ns

254 newname sname lhs rhs in

258 newname sname lhs rhs in

255 newpats where

259 newpats where

256

260

@@ -269,8 +273,10 @@ mkPE_TermDecl ist newname sname ns

269 deImpArg a = a

273 deImpArg a = a

270

274

271-- | Get specialised applications for a given function

275-- | Get specialised applications for a given function

272−getSpecApps :: IState -> [Name] -> Term ->

276+getSpecApps :: IState

277+ -> [Name]

278+ -> Term

273− [(Name, [(PEArgType, Term)])]

279+ -> [(Name, [(PEArgType, Term)])]

274getSpecApps ist env tm = ga env (explicitNames tm) where

280getSpecApps ist env tm = ga env (explicitNames tm) where

275

281

276-- staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)

282-- staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)

@@ -326,7 +332,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

326

332

327 -- There's an overlap if the case tree has a default case along with

333 -- There's an overlap if the case tree has a default case along with

328 -- some other cases. It's fine if there's a default case on its own.

334 -- some other cases. It's fine if there's a default case on its own.

329− noOverlapAlts (ConCase _ _ _ sc : rest)

335+ noOverlapAlts (ConCase _ _ _ sc : rest)

330 = noOverlapAlts rest && noOverlap sc

336 = noOverlapAlts rest && noOverlap sc

331 noOverlapAlts (FnCase _ _ sc : rest) = noOverlapAlts rest

337 noOverlapAlts (FnCase _ _ sc : rest) = noOverlapAlts rest

332 noOverlapAlts (ConstCase _ sc : rest)

338 noOverlapAlts (ConstCase _ sc : rest)

@@ -335,4 +341,3 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

335 = noOverlapAlts rest && noOverlap sc

341 = noOverlapAlts rest && noOverlap sc

336 noOverlapAlts (DefaultCase _ : _) = False

342 noOverlapAlts (DefaultCase _ : _) = False

337 noOverlapAlts _ = True

343 noOverlapAlts _ = True

338−

src/Idris/ProofSearch.hs+21−19

@@ -113,17 +113,18 @@ cantSolveGoal = do g <- goal

113 lift $ tfail $

114 CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)

115

116−proofSearch :: Bool -> -- recursive search (False for 'refine')

116+proofSearch :: Bool -- ^ recursive search (False for 'refine')

117− Bool -> -- invoked from a tactic proof. If so, making

117+ -> Bool -- ^ invoked from a tactic proof. If so, making new metavariables is meaningless, and there should be an error reported instead.

118− -- new metavariables is meaningless, and there shoudl

119− -- be an error reported instead.

120− Bool -> -- ambiguity ok

118+ -> Bool -- ^ ambiguity ok

121− Bool -> -- defer on failure

119+ -> Bool -- ^ defer on failure

122− Int -> -- maximum depth

120+ -> Int -- ^ maximum depth

123− (PTerm -> ElabD ()) -> Maybe Name -> Name ->

121+ -> (PTerm -> ElabD ())

122+ -> Maybe Name

123+ -> Name

124− [Name] ->

124+ -> [Name]

125− [Name] ->

125+ -> [Name]

126− IState -> ElabD ()

126+ -> IState

127+ -> ElabD ()

127proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist

128proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist

128 = do -- get all possible versions of the name, take the first one that

129 = do -- get all possible versions of the name, take the first one that

129 -- works

130 -- works

@@ -336,13 +337,14 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

336 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]

337 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]

337 _ -> []

338 _ -> []

338

339

339−-- | Resolve interfaces. This will only pick up 'normal' implementations, never

340+-- | Resolve interfaces. This will only pick up 'normal'

340−-- named implementations (which is enforced by 'findInstances').

341+-- implementations, never named implementations (which is enforced by

342+-- 'findInstances').

341−resolveTC :: Bool -- ^ using default Int

343+resolveTC :: Bool -- ^ using default Int

342− -> Bool -- ^ allow open implementations

344+ -> Bool -- ^ allow open implementations

343− -> Int -- ^ depth

345+ -> Int -- ^ depth

344− -> Term -- ^ top level goal, for error messages

346+ -> Term -- ^ top level goal, for error messages

345− -> Name -- ^ top level function name, to prevent loops

347+ -> Name -- ^ top level function name, to prevent loops

346 -> (PTerm -> ElabD ()) -- ^ top level elaborator

348 -> (PTerm -> ElabD ()) -- ^ top level elaborator

347 -> IState -> ElabD ()

349 -> IState -> ElabD ()

348resolveTC def openOK depth top fn elab ist

350resolveTC def openOK depth top fn elab ist

@@ -392,7 +394,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

392 try' (trivialTCs okholes elab ist)

394 try' (trivialTCs okholes elab ist)

393 (do addDefault t tc ttypes

395 (do addDefault t tc ttypes

394 let stk = map fst (filter snd $ elab_stack ist)

396 let stk = map fst (filter snd $ elab_stack ist)

395− let insts = idris_openimpls ist ++ findInstances ist t

397+ let insts = idris_openimpls ist ++ findInstances ist t

396 blunderbuss t depth stk (stk ++ insts)) True

398 blunderbuss t depth stk (stk ++ insts)) True

397

399

398 -- returns Just hs if okay, where hs are holes which are okay in the

400 -- returns Just hs if okay, where hs are holes which are okay in the

src/Idris/Transforms.hs+17−19

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.Transforms(transformPats,

3+module Idris.Transforms(transformPats,

4 transformPatsWith,

5 applyTransRulesWith,

6 applyTransRules) where

@@ -27,23 +27,23 @@ transformPatsWith rs ps = map tClause ps where

27 = let rhs' = applyTransRulesWith rs rhs in

28 Right (lhs, rhs')

30−-- Work on explicitly named terms, so we don't have to manipulate

30+-- | Work on explicitly named terms, so we don't have to manipulate de

31−-- de Bruijn indices

31+-- Bruijn indices

32applyTransRules :: IState -> Term -> Term

33applyTransRules ist tm = finalise $ applyAll [] (idris_transforms ist) (vToP tm)

35−-- Work on explicitly named terms, so we don't have to manipulate

35+-- | Work on explicitly named terms, so we don't have to manipulate de

36−-- de Bruijn indices

36+-- Bruijn indices

37applyTransRulesWith :: [(Term, Term)] -> Term -> Term

38−applyTransRulesWith rules tm

38+applyTransRulesWith rules tm

39 = finalise $ applyAll rules emptyContext (vToP tm)

41applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term

42−applyAll extra ts ap@(App s f a)

42+applyAll extra ts ap@(App s f a)

43 | (P _ fn ty, args) <- unApply ap

44 = let rules = case lookupCtxtExact fn ts of

45 Just r -> extra ++ r

46− Nothing -> extra

46+ Nothing -> extra

47 ap' = App s (applyAll extra ts f) (applyAll extra ts a) in

48 case rules of

49 [] -> ap'

@@ -52,9 +52,9 @@ applyAll extra ts ap@(App s f a)

52 App s (applyAll extra ts f')

53 (applyAll extra ts a')

54 Just tm' -> tm'

55− _ -> App s (applyAll extra ts f)

55+ _ -> App s (applyAll extra ts f)

56 (applyAll extra ts a)

57−applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

57+applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

58 (applyAll extra ts sc)

59applyAll extra ts t = t

@@ -64,11 +64,11 @@ applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'

64 | otherwise = applyFnRules rs tm

66applyRule :: (Term, Term) -> Term -> Maybe Term

67−applyRule (lhs, rhs) tm

67+applyRule (lhs, rhs) tm

68− | Just ms <- matchTerm lhs tm

68+ | Just ms <- matchTerm lhs tm

69-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++

70−-- "\n" ++ show rhs

70+-- "\n" ++ show rhs

71−-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $

71+-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $

72 = Just $ depat ms rhs

73 | otherwise = Nothing

74-- ASSUMPTION: The names in the transformation rule bindings cannot occur

@@ -76,7 +76,7 @@ applyRule (lhs, rhs) tm

76-- (In general, this would not be true, but when we elaborate transformation

77-- rules we mangle the names so that it is true. While this feels a bit

78-- hacky, it's much easier to think about than mangling de Bruijn indices).

79− where depat ms (Bind n (PVar t) sc)

79+ where depat ms (Bind n (PVar t) sc)

80 = case lookup n ms of

81 Just tm -> depat ms (subst n tm sc)

82 _ -> depat ms sc -- no occurrence? Shouldn't happen

@@ -85,9 +85,9 @@ applyRule (lhs, rhs) tm

85matchTerm :: Term -> Term -> Maybe [(Name, Term)]

86matchTerm lhs tm = matchVars [] lhs tm

87 where

88− matchVars acc (Bind n (PVar t) sc) tm

88+ matchVars acc (Bind n (PVar t) sc) tm

89 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm

90− matchVars acc sc tm

90+ matchVars acc sc tm

91 = -- trace (show acc ++ ": " ++ show (sc, tm)) $

92 doMatch acc sc tm

@@ -100,5 +100,3 @@ matchTerm lhs tm = matchVars [] lhs tm

100 return (fm ++ am)

101 doMatch ns x y | vToP x == vToP y = return []

102 | otherwise = Nothing

103−

104−