be0ff0f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add 'definable' flag to metavariables

A metavariable is definable if it appears in a function with no hole bindings yet to be inferred. We don't use this yet, but it will allow us more flexibility in using holes where the solution will solve other metavariables.

commitbe0ff0f81b2e7a130871571a6a6923c2f61e52df authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 25 Feb 2016, 11:55 (11 years ago) parent65125ae

12 files changed+33−29

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4−3 src/Idris/AbsSyntaxTree.hs+5−3 src/Idris/Completion.hs+1−1 src/Idris/Delaborate.hs+2−2 src/Idris/Elab/Clause.hs+4−4 src/Idris/Elab/Term.hs+1−1 src/Idris/Elab/Type.hs+1−1 src/Idris/Elab/Utils.hs+1−1 src/Idris/Elab/Value.hs+1−1 src/Idris/IBC.hs+3−3 src/Idris/Interactive.hs+4−4 src/Idris/REPL.hs+6−5

src/Idris/AbsSyntax.hs+4−3

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

646646

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

648648addDeferred' :: NameType

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

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

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

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

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

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

655655 -- allowed

656656 -> Idris ()

657657addDeferred' 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

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

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

662663 idris_metavars i }

663664 where

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

src/Idris/AbsSyntaxTree.hs+5−3

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

211211 idris_name :: Int,

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

213213 -- ^ 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))],

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

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

217217 -- 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

219− -- allowed

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

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)

220222 idris_coercions :: [Name],

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

222224 syntax_rules :: SyntaxRules,

src/Idris/Completion.hs+1−1

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

5252

5353metavars :: Idris [String]

5454metavars = 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

5656

5757

5858modules :: Idris [String]

src/Idris/Delaborate.hs+2−2

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

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

107107 | otherwise

108108 = case lookup n (idris_metavars ist) of

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

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

110110 _ -> PRef un [] n

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

112112 = 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

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

173173 deFn env (P _ n _) args

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

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

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

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

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

178178 | 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

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

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

701701 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'

703703 addDeferred def''

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

705705

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

862862 sendHighlighting highlights

863863

864864 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'

866866 addDeferred def''

867867 mapM_ (elabCaseBlock info opts) is

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

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

927927 addIBC (IBCStatic wname)

928928

929929 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'

931931 addDeferred def''

932932

933933 -- in the subdecls, lhs becomes:

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

968968 sendHighlighting highlights

969969

970970 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'

972972 addDeferred def''

973973 mapM_ (elabCaseBlock info opts) is

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

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

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

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

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

25192519 -- 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

25212521 in addDeferred ds'

25222522 _ -> return ()

25232523 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

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

177177 addIBC (IBCDef n)

178178 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

180180 addDeferred ds'

181181 setFlags n opts'

182182 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)

6868 = do ctxt <- getContext

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

7070 (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))]

7272 addIBC (IBCDef n)

7373 ns' <- checkAddDef add toplvl fc mkerr ns

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

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

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

7676 let vtm = orderPats (getInferTerm tm')

7777

7878 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'

8080 addDeferred def''

8181 mapM_ (elabCaseBlock info []) is

8282

src/Idris/IBC.hs+3−3

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 135

43+ibcVersion = 136

4444

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

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

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

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

8585 ibc_errorhandlers :: ![Name],

8686 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))],

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

8989 ibc_postulates :: ![Name],

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

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

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

663663 addFunctionErrorHandlers fn arg [handler]) ns

664664

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

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

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

667667

668668----- For Cheapskate and docstrings

src/Idris/Interactive.hs+4−4

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

230230 [] -> return n

231231 ns -> ierror (CantResolveAlts ns)

232232 i <- getIState

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

233+ let (top, envlen, psnames)

234234 = case lookup mn (idris_metavars i) of

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

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

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

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

237237 let fc = fileFC fn

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

239239 (ProofSearch rec False depth t psnames hints)]

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

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

333333 i <- getIState

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

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

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

336336 _ -> return (-1)

337337

338338 if (not isProv) then do

src/Idris/REPL.hs+6−5

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

959959 case lookupNames n ctxt of

960960 ts@(t:_) ->

961961 case lookup t (idris_metavars ist) of

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

963− showMetavarInfo ppo ist n i

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

963+ showMetavarInfo ppo ist n i

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

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

966966 where

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

11391139 insertMetavar n =

11401140 do i <- getIState

11411141 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 }

11431143

11441144process fn' (AddProof prf)

11451145 = do fn <- do

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

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

11931193 n <- case metavars of

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

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

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

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

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

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

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

11981199 prover mode (lit fn) n

11991200 -- recheck totality