mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 18:02:24 +03:00
More flexible holes
Holes can now depend on other holes (e.g. hole bindings in a term which will be inferred from the solution of the hole). However, holes with dependencies can only be inspected, not defined later, since the later definition won't solve those remaining implicit arguments.
This commit is contained in:
parent
be0ff0f81b
commit
76c46bb770
@ -60,6 +60,9 @@ Minor language changes
|
||||
* File Modes expanded: Append, ReadWriteTruncate, and ReadAppend added,
|
||||
Write is deprecated and renamed to WriteTruncate.
|
||||
* C11 Extended Mode variations added to File Modes.
|
||||
* More flexible holes.
|
||||
Holes can now depend on other holes in a term (such as implicit arguments
|
||||
which may be inferred from the definition of the hole).
|
||||
|
||||
New in 0.10:
|
||||
============
|
||||
|
@ -672,9 +672,13 @@ addDeferred' nt ns
|
||||
Bind n' b $ tidyNames (S.insert n' used) sc
|
||||
tidyNames used b = b
|
||||
|
||||
solveDeferred :: Name -> Idris ()
|
||||
solveDeferred n = do i <- getIState
|
||||
putIState $ i { idris_metavars =
|
||||
solveDeferred :: FC -> Name -> Idris ()
|
||||
solveDeferred fc n
|
||||
= do i <- getIState
|
||||
case lookup n (idris_metavars i) of
|
||||
Just (_, _, _, _, False) ->
|
||||
throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
|
||||
_ -> putIState $ i { idris_metavars =
|
||||
filter (\(n', _) -> n/=n')
|
||||
(idris_metavars i),
|
||||
ibc_write =
|
||||
|
@ -87,7 +87,7 @@ elabClauses info' fc opts n_in cs =
|
||||
let pats_raw = map (simple_lhs ctxt) pats_in
|
||||
logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw
|
||||
|
||||
solveDeferred n
|
||||
solveDeferred fc n
|
||||
|
||||
-- just ensure that the structure exists
|
||||
fmodifyState (ist_optimisation n) id
|
||||
@ -670,7 +670,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
|
||||
ctxt <- getContext -- new context with where block added
|
||||
logElab 5 "STARTING CHECK"
|
||||
((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-
|
||||
((rhs', defer, holes, is, probs, ctxt', newDecls, highlights), _) <-
|
||||
tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState
|
||||
(do pbinds ist lhs_tm
|
||||
-- proof search can use explicitly written names
|
||||
@ -687,7 +687,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
let (tm, ds) = runState (collectDeferred (Just fname)
|
||||
(map fst $ case_decls aux) ctxt tt) []
|
||||
probs <- get_probs
|
||||
return (tm, ds, is, probs, ctxt', newDecls, highlights))
|
||||
hs <- get_holes
|
||||
return (tm, ds, hs, is, probs, ctxt', newDecls, highlights))
|
||||
setContext ctxt'
|
||||
processTacticDecls info newDecls
|
||||
sendHighlighting highlights
|
||||
@ -698,9 +699,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
logElab 4 $ "---> " ++ show rhs'
|
||||
when (not (null defer)) $ logElab 1 $ "DEFERRED " ++
|
||||
show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
|
||||
def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) defer
|
||||
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
|
||||
|
||||
-- If there's holes, set the metavariables as undefinable
|
||||
def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer
|
||||
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, null holes))) def'
|
||||
addDeferred def''
|
||||
|
||||
mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
|
||||
|
||||
when (not (null def')) $ do
|
||||
@ -716,11 +720,23 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
logElab 5 $ "Rechecking"
|
||||
logElab 6 $ " ==> " ++ show (forget rhs')
|
||||
|
||||
(crhs, crhsty) <- if not inf
|
||||
then recheckC_borrowing True (PEGenerated `notElem` opts)
|
||||
borrowed fc id [] rhs'
|
||||
else return (rhs', clhsty)
|
||||
(crhs, crhsty) -- if there's holes && deferred things, it's okay
|
||||
-- but we'll need to freeze the definition and not
|
||||
-- allow the deferred things to be definable
|
||||
-- (this is just to allow users to inspect intermediate
|
||||
-- things)
|
||||
<- if (null holes || null def') && not inf
|
||||
then recheckC_borrowing True (PEGenerated `notElem` opts)
|
||||
borrowed fc id [] rhs'
|
||||
else return (rhs', clhsty)
|
||||
|
||||
logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty
|
||||
|
||||
-- If there's holes, make sure this definition is frozen
|
||||
when (not (null holes)) $ do
|
||||
logElab 5 $ "Making " ++ show fname ++ " frozen due to " ++ show holes
|
||||
setAccessibility fname Frozen
|
||||
|
||||
ctxt <- getContext
|
||||
let constv = next_tvar ctxt
|
||||
case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
|
||||
@ -861,7 +877,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
processTacticDecls info newDecls
|
||||
sendHighlighting highlights
|
||||
|
||||
def' <- checkDef fc iderr defer
|
||||
def' <- checkDef fc iderr True defer
|
||||
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
|
||||
addDeferred def''
|
||||
mapM_ (elabCaseBlock info opts) is
|
||||
@ -926,7 +942,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
addIBC (IBCImp wname)
|
||||
addIBC (IBCStatic wname)
|
||||
|
||||
def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]
|
||||
def' <- checkDef fc iderr True [(wname, (-1, Nothing, wtype, []))]
|
||||
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
|
||||
addDeferred def''
|
||||
|
||||
@ -967,7 +983,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
processTacticDecls info newDecls
|
||||
sendHighlighting highlights
|
||||
|
||||
def' <- checkDef fc iderr defer
|
||||
def' <- checkDef fc iderr True defer
|
||||
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
|
||||
addDeferred def''
|
||||
mapM_ (elabCaseBlock info opts) is
|
||||
|
@ -355,7 +355,7 @@ elabCaseFun ind paramPos n ty cons info = do
|
||||
(ierror . Elaborating "type declaration of " elimDeclName Nothing)
|
||||
-- Do not elaborate clauses if there aren't any
|
||||
case eliminatorClauses of
|
||||
[] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
|
||||
[] -> State.lift $ solveDeferred emptyFC elimDeclName -- Remove meta-variable for type
|
||||
_ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
|
||||
(ierror . Elaborating "clauses of " elimDeclName Nothing)
|
||||
where elimLog :: String -> EliminatorState ()
|
||||
|
@ -2508,7 +2508,7 @@ processTacticDecls info steps =
|
||||
updateIState $ \i -> i { idris_implicits =
|
||||
addDef n impls (idris_implicits i) }
|
||||
addIBC (IBCImp n)
|
||||
ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))]
|
||||
ds <- checkDef fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]
|
||||
addIBC (IBCDef n)
|
||||
ctxt <- getContext
|
||||
case lookupDef n ctxt of
|
||||
@ -2528,7 +2528,7 @@ processTacticDecls info steps =
|
||||
addIBC (IBCInstance False True className instName)
|
||||
RClausesInstrs n cs ->
|
||||
do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
|
||||
solveDeferred n
|
||||
solveDeferred emptyFC n
|
||||
let lhss = map (\(_, lhs, _) -> lhs) cs
|
||||
let fc = fileFC "elab_reflected"
|
||||
pmissing <-
|
||||
|
@ -78,7 +78,7 @@ buildType info syn fc opts n ty' = do
|
||||
|
||||
logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'
|
||||
|
||||
ds <- checkAddDef True False fc iderr defer
|
||||
ds <- checkAddDef True False fc iderr True defer
|
||||
-- if the type is not complete, note that we'll need to infer
|
||||
-- things later (for solving metavariables)
|
||||
when (length ds > length is) -- more deferred than case blocks
|
||||
@ -173,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
|
||||
-- Productivity checking now via checking for guarded 'Delay'
|
||||
let opts' = opts -- if corec then (Coinductive : opts) else opts
|
||||
let usety = if norm then nty' else nty
|
||||
ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]
|
||||
ds <- checkDef fc iderr True [(n, (-1, Nothing, usety, []))]
|
||||
addIBC (IBCDef n)
|
||||
addDefinedName n
|
||||
let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds
|
||||
@ -255,7 +255,7 @@ elabPostulate info syn doc fc nfc opts n ty = do
|
||||
sendHighlighting [(nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]
|
||||
|
||||
-- remove it from the deferred definitions list
|
||||
solveDeferred n
|
||||
solveDeferred fc n
|
||||
|
||||
elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
|
||||
FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
|
||||
@ -268,4 +268,4 @@ elabExtern info syn doc fc nfc opts n ty = do
|
||||
addIBC (IBCExtern (n, arity))
|
||||
|
||||
-- remove it from the deferred definitions list
|
||||
solveDeferred n
|
||||
solveDeferred fc n
|
||||
|
@ -56,21 +56,23 @@ checkDeprecated fc n
|
||||
iderr :: Name -> Err -> Err
|
||||
iderr _ e = e
|
||||
|
||||
checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))]
|
||||
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
|
||||
checkDef fc mkerr ns = checkAddDef False True fc mkerr ns
|
||||
checkDef :: FC -> (Name -> Err -> Err) -> Bool ->
|
||||
[(Name, (Int, Maybe Name, Type, [Name]))] ->
|
||||
Idris [(Name, (Int, Maybe Name, Type, [Name]))]
|
||||
checkDef fc mkerr definable ns
|
||||
= checkAddDef False True fc mkerr definable ns
|
||||
|
||||
checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
|
||||
checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> Bool
|
||||
-> [(Name, (Int, Maybe Name, Type, [Name]))]
|
||||
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
|
||||
checkAddDef add toplvl fc mkerr [] = return []
|
||||
checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)
|
||||
checkAddDef add toplvl fc mkerr def [] = return []
|
||||
checkAddDef add toplvl fc mkerr definable ((n, (i, top, t, psns)) : ns)
|
||||
= do ctxt <- getContext
|
||||
logElab 5 $ "Rechecking deferred name " ++ show (n, t)
|
||||
logElab 5 $ "Rechecking deferred name " ++ show (n, t, definable)
|
||||
(t', _) <- recheckC fc (mkerr n) [] t
|
||||
when add $ do addDeferred [(n, (i, top, t, psns, toplvl, True))]
|
||||
when add $ do addDeferred [(n, (i, top, t, psns, toplvl, definable))]
|
||||
addIBC (IBCDef n)
|
||||
ns' <- checkAddDef add toplvl fc mkerr ns
|
||||
ns' <- checkAddDef add toplvl fc mkerr definable ns
|
||||
return ((n, (i, top, t', psns)) : ns')
|
||||
|
||||
-- | Get the list of (index, name) of inaccessible arguments from an elaborated
|
||||
|
@ -75,7 +75,7 @@ elabValBind info aspat norm tm_in
|
||||
|
||||
let vtm = orderPats (getInferTerm tm')
|
||||
|
||||
def' <- checkDef (fileFC "(input)") iderr defer
|
||||
def' <- checkDef (fileFC "(input)") iderr True defer
|
||||
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) def'
|
||||
addDeferred def''
|
||||
mapM_ (elabCaseBlock info []) is
|
||||
|
@ -533,7 +533,7 @@ pDefs reexp ds
|
||||
case d' of
|
||||
TyDecl _ _ -> return ()
|
||||
_ -> do logIBC 1 $ "SOLVING " ++ show n
|
||||
solveDeferred n
|
||||
solveDeferred emptyFC n
|
||||
updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })
|
||||
) ds
|
||||
where
|
||||
|
@ -124,7 +124,7 @@ prove mode opt ctxt lit n ty
|
||||
[([], P Ref n ty, ptm')] ty
|
||||
ctxt
|
||||
setContext ctxt'
|
||||
solveDeferred n
|
||||
solveDeferred emptyFC n
|
||||
case idris_outputmode i of
|
||||
IdeMode n h ->
|
||||
runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n
|
||||
|
Loading…
Reference in New Issue
Block a user