be0ff0f · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+4−3

compare with master

unifiedsplit

@@ -646,7 +646,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

646

647-- | Save information about a name that is not yet defined

648addDeferred' :: NameType

649− -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]

649+ -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]

650 -- ^ The Name is the name being made into a metavar,

651 -- the Int is the number of vars that are part of a

652 -- putative proof context, the Maybe Name is the

@@ -655,10 +655,11 @@ addDeferred' :: NameType

655 -- allowed

656 -> Idris ()

657addDeferred' nt ns

658− = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

658+ = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

659 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

660 i <- getIState

661− putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++

661+ putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->

662+ (n, (top, i, ns, isTopLevel, isDefinable))) ns ++

662 idris_metavars i }

663 idris_metavars i }

663 where

664 where

664 -- 'tidyNames' is to generate user accessible names in case they are

665 -- 'tidyNames' is to generate user accessible names in case they are

src/Idris/AbsSyntaxTree.hs+5−3

@@ -211,12 +211,14 @@ data IState = IState {

211 idris_name :: Int,

212 idris_lineapps :: [((FilePath, Int), PTerm)],

213 -- ^ Full application LHS on source line

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

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

215 -- ^ The currently defined but not proven metavariables. The Int

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

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

218− -- available for proof search and the Bool is whether :p is

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

219− -- allowed

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

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

221+ -- still has hole bindings)

220 idris_coercions :: [Name],

222 idris_coercions :: [Name],

221 idris_errRev :: [(Term, Term)],

223 idris_errRev :: [(Term, Term)],

222 syntax_rules :: SyntaxRules,

224 syntax_rules :: SyntaxRules,

src/Idris/Completion.hs+1−1

@@ -52,7 +52,7 @@ names = do i <- get

52

53metavars :: Idris [String]

54metavars = do i <- get

55− return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t)) -> not t) (idris_metavars i)) \\ primDefs

55+ return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs

56

57

58modules :: Idris [String]

src/Idris/Delaborate.hs+2−2

@@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

106 | Just n' <- lookup n env = PRef un [] n'

107 | otherwise

108 = case lookup n (idris_metavars ist) of

109− Just (Just _, mi, _, _) -> mkMVApp n []

109+ Just (Just _, mi, _, _, _) -> mkMVApp n []

110 _ -> PRef un [] n

111 de env _ (Bind n (Lam ty) sc)

112 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

@@ -172,7 +172,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

172 = PApp un (de env [] f) (map pexp (map (de env []) args))

173 deFn env (P _ n _) args

174 | not mvs = case lookup n (idris_metavars ist) of

175− Just (Just _, mi, _, _) ->

175+ Just (Just _, mi, _, _, _) ->

176 mkMVApp n (drop mi (map (de env []) args))

177 _ -> mkPApp n (map (de env []) args)

178 | otherwise = mkPApp n (map (de env []) args)

src/Idris/Elab/Clause.hs+4−4

@@ -699,7 +699,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

699 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++

700 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

701 def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) defer

702− let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

702+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

703 addDeferred def''

704 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

705

@@ -862,7 +862,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

862 sendHighlighting highlights

863

864 def' <- checkDef fc iderr defer

865− let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

865+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

866 addDeferred def''

867 mapM_ (elabCaseBlock info opts) is

868 logElab 5 ("Checked wval " ++ show wval')

@@ -927,7 +927,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

927 addIBC (IBCStatic wname)

928

929 def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]

930− let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

930+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

931 addDeferred def''

932

933 -- in the subdecls, lhs becomes:

@@ -968,7 +968,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

968 sendHighlighting highlights

969

970 def' <- checkDef fc iderr defer

971− let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

971+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

972 addDeferred def''

973 mapM_ (elabCaseBlock info opts) is

974 logElab 5 ("Checked RHS " ++ show rhs')

src/Idris/Elab/Term.hs+1−1

@@ -2517,7 +2517,7 @@ processTacticDecls info steps =

2517 -- then it must be added as a metavariable. This needs guarding

2518 -- to prevent overwriting case defs with a metavar, if the case

2519 -- defs come after the type decl in the same script!

2520− let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds

2520+ let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds

2521 in addDeferred ds'

2522 _ -> return ()

2523 RAddInstance className instName ->

src/Idris/Elab/Type.hs+1−1

@@ -176,7 +176,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

176 ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]

177 addIBC (IBCDef n)

178 addDefinedName n

179− let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds

179+ let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds

180 addDeferred ds'

181 setFlags n opts'

182 checkDocs fc argDocs ty

src/Idris/Elab/Utils.hs+1−1

@@ -68,7 +68,7 @@ checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)

68 = do ctxt <- getContext

69 logElab 5 $ "Rechecking deferred name " ++ show (n, t)

70 (t', _) <- recheckC fc (mkerr n) [] t

71− when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]

71+ when add $ do addDeferred [(n, (i, top, t, psns, toplvl, True))]

72 addIBC (IBCDef n)

73 ns' <- checkAddDef add toplvl fc mkerr ns

74 return ((n, (i, top, t', psns)) : ns')

src/Idris/Elab/Value.hs+1−1

@@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in

76 let vtm = orderPats (getInferTerm tm')

77

78 def' <- checkDef (fileFC "(input)") iderr defer

79− let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) def'

79+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) def'

80 addDeferred def''

81 mapM_ (elabCaseBlock info []) is

82

src/Idris/IBC.hs+3−3

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 135

43+ibcVersion = 136

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

@@ -84,7 +84,7 @@ data IBCFile = IBCFile { ver :: Word16,

84 ibc_metainformation :: ![(Name, MetaInformation)],

85 ibc_errorhandlers :: ![Name],

86 ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler

87− ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],

87+ ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool, Bool))],

88 ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))],

89 ibc_postulates :: ![Name],

90 ibc_externs :: ![(Name, Int)],

@@ -662,7 +662,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

662pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->

663 addFunctionErrorHandlers fn arg [handler]) ns

664

665−pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris ()

665+pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> Idris ()

666pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

667

668----- For Cheapskate and docstrings

src/Idris/Interactive.hs+4−4

@@ -230,10 +230,10 @@ doProofSearch fn updatefile rec l n hints (Just depth)

230 [] -> return n

231 ns -> ierror (CantResolveAlts ns)

232 i <- getIState

233− let (top, envlen, psnames, _)

233+ let (top, envlen, psnames)

234 = case lookup mn (idris_metavars i) of

235− Just (t, e, ns, False) -> (t, e, ns, False)

235+ Just (t, e, ns, False, d) -> (t, e, ns)

236− _ -> (Nothing, 0, [], True)

236+ _ -> (Nothing, 0, [])

237 let fc = fileFC fn

238 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))

239 (ProofSearch rec False depth t psnames hints)]

@@ -332,7 +332,7 @@ makeLemma fn updatefile l n

332 ns -> ierror (CantResolveAlts (map fst ns))

333 i <- getIState

334 margs <- case lookup fname (idris_metavars i) of

335− Just (_, arity, _, _) -> return arity

335+ Just (_, arity, _, _, _) -> return arity

336 _ -> return (-1)

337

338 if (not isProv) then do

src/Idris/REPL.hs+6−5

@@ -959,8 +959,8 @@ process fn (Check (PRef _ _ n))

959 case lookupNames n ctxt of

960 ts@(t:_) ->

961 case lookup t (idris_metavars ist) of

962− Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

962+ Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

963− showMetavarInfo ppo ist n i

963+ showMetavarInfo ppo ist n i

964 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

965 [] -> iPrintError $ "No such variable " ++ show n

966 where

@@ -1139,7 +1139,7 @@ process fn (RmProof n')

1139 insertMetavar n =

1140 do i <- getIState

1141 let ms = idris_metavars i

1142− putIState $ i { idris_metavars = (n, (Nothing, 0, [], False)) : ms }

1142+ putIState $ i { idris_metavars = (n, (Nothing, 0, [], False, False)) : ms }

1143

1144process fn' (AddProof prf)

1145 = do fn <- do

@@ -1192,8 +1192,9 @@ process fn (Prove mode n')

1192 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns

1193 n <- case metavars of

1194 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

1195− [(n, (_,_,_,False))] -> return n

1195+ [(n, (_,_,_,False,_))] -> return n

1196+ [(_, (_,_,_,_,False))] -> ierror (Msg $ "Can't prove this hole as it depends on other holes")

1196− [(_, (_,_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1197+ [(_, (_,_,_,True,_))] -> ierror (Msg $ "Declarations not solvable using prover")

1197 ns -> ierror (CantResolveAlts (map fst ns))

1198 ns -> ierror (CantResolveAlts (map fst ns))

1198 prover mode (lit fn) n

1199 prover mode (lit fn) n

1199 -- recheck totality

1200 -- recheck totality