ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 05:57:38 +03:00
Code Issues Projects Releases Wiki Activity

Proof search should only use user visible names

Browse Source 
If they are implicits or class arguments, it's fine for 'auto' to see
them since they're only used internally, but interactive proof search
will give odd results if it uses them. So, we make a list of names which
proof search in interactive mode is allowed to use.
This commit is contained in:
Edwin Brady 2015-08-01 21:12:14 +01:00
parent 8dd2a7f078
commit 7095d6c1ed
27 changed files with 150 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Idris/AbsSyntax.hs
View File

@ -597,7 +597,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)
-- | Save information about a name that is not yet defined
addDeferred' :: NameType
-> [(Name, (Int, Maybe Name, Type, Bool))]
-> [(Name, (Int, Maybe Name, Type, [Name], Bool))]
-- ^ The Name is the name being made into a metavar,
-- the Int is the number of vars that are part of a
-- putative proof context, the Maybe Name is the
@ -606,10 +606,10 @@ addDeferred' :: NameType
-- allowed
-> Idris ()
addDeferred' nt ns
= do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
= do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
i <- getIState
putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++
idris_metavars i }
where
-- 'tidyNames' is to generate user accessible names in case they are

19
src/Idris/AbsSyntaxTree.hs
View File

@ -195,10 +195,11 @@ data IState = IState {
idris_name :: Int,
idris_lineapps :: [((FilePath, Int), PTerm)],
-- ^ Full application LHS on source line
idris_metavars :: [(Name, (Maybe Name, Int, Bool))],
idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],
-- ^ The currently defined but not proven metavariables. The Int
-- is the number of vars to display as a context, the Maybe Name
-- is its top-level function, and the Bool is whether :p is
-- is its top-level function, the [Name] is the list of local variables
-- available for proof search and the Bool is whether :p is
-- allowed
idris_coercions :: [Name],
idris_errRev :: [(Term, Term)],
@ -404,9 +405,11 @@ data Command = Quit
| MakeWith Bool Int Name
| MakeCase Bool Int Name
| MakeLemma Bool Int Name
| DoProofSearch Bool Bool Int Name [Name]
-- ^ the first bool is whether to update,
-- the second is whether to search recursively (i.e. for the arguments)
| DoProofSearch Bool -- update file
Bool -- recursive search
Int -- depth
Name -- top level name
[Name] -- hints
| SetOpt Opt
| UnsetOpt Opt
| NOP
@ -982,7 +985,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
| MatchRefine Name
| LetTac Name t | LetTacTy Name t t
| Exact t | Compute | Trivial | TCInstance
| ProofSearch Bool Bool Int (Maybe Name) [Name]
| ProofSearch Bool Bool Int (Maybe Name)
[Name] -- allowed local names
[Name] -- hints
-- ^ the bool is whether to search recursively
| Solve
| Attack
@ -1580,7 +1585,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
depth d . bracket p startPrec $
prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

2
src/Idris/Completion.hs
View File

@ -52,7 +52,7 @@ names = do i <- get
metavars :: Idris [String]
metavars = do i <- get
return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
modules :: Idris [String]

10
src/Idris/Core/Binary.hs
View File

@ -499,9 +499,10 @@ instance (Binary b) => Binary (Binder b) where
put x2
Hole x1 -> do putWord8 4
put x1
GHole x1 x2 -> do putWord8 5
put x1
put x2
GHole x1 x2 x3 -> do putWord8 5
put x1
put x2
put x3
Guess x1 x2 -> do putWord8 6
put x1
put x2
@ -528,7 +529,8 @@ instance (Binary b) => Binary (Binder b) where
return (Hole x1)
5 -> do x1 <- get
x2 <- get
return (GHole x1 x2)
x3 <- get
return (GHole x1 x2 x3)
6 -> do x1 <- get
x2 <- get
return (Guess x1 x2)

2
src/Idris/Core/DeepSeq.hs
View File

@ -128,7 +128,7 @@ instance (NFData b) => NFData (Binder b) where
rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (Hole x1) = rnf x1 `seq` ()
rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (PVar x1) = rnf x1 `seq` ()
rnf (PVTy x1) = rnf x1 `seq` ()

14
src/Idris/Core/Elaborate.hs
View File

@ -51,6 +51,20 @@ explicit n = do ES (p, a) s m <- get
let p' = p { dontunify = n : dontunify p }
put (ES (p', a) s m)
-- Add a name that's okay to use in proof search (typically either because
-- it was given explicitly on the lhs, or intrduced as an explicit lambda
-- or let binding)
addPSname :: Name -> Elab' aux ()
addPSname n@(UN _)
= do ES (p, a) s m <- get
let p' = p { psnames = n : psnames p }
put (ES (p', a) s m)
addPSname _ = return () -- can only use user given names
getPSnames :: Elab' aux [Name]
getPSnames = do ES (p, a) s m <- get
return (psnames p)
saveState :: Elab' aux ()
saveState = do e@(ES p s _) <- get
put (ES p s (Just e))

2
src/Idris/Core/Execute.hs
View File

@ -93,7 +93,7 @@ toTT (EBind n b body) = do n' <- newN n
fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
fixBinder (Hole t) = Hole <$> toTT t
fixBinder (GHole i t) = GHole i <$> toTT t
fixBinder (GHole i ns t) = GHole i ns <$> toTT t
fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
fixBinder (PVar t) = PVar <$> toTT t
fixBinder (PVTy t) = PVTy <$> toTT t

8
src/Idris/Core/ProofState.hs
View File

@ -39,6 +39,7 @@ data ProofState = PS { thname :: Name,
deferred :: [Name], -- ^ names we'll need to define
instances :: [Name], -- ^ instance arguments (for type classes)
autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes
psnames :: [Name], -- ^ Local names okay to use in proof search
previous :: Maybe ProofState, -- ^ for undo
context :: Context,
datatypes :: Ctxt TypeInfo,
@ -301,7 +302,7 @@ newProof n ctxt datatypes ty =
in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
(P Bound h ty'))) ty [] (h, []) [] []
Nothing [] []
[] [] []
[] [] [] []
Nothing ctxt datatypes "" False False [] []
type TState = ProofState -- [TacticAction])
@ -429,7 +430,8 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
do let env' = filter (\(n, t) -> n `notElem` dropped) env
action (\ps -> let hs = holes ps in
ps { holes = hs \\ [x] })
return (Bind n (GHole (length env') (mkTy (reverse env') t))
ps <- get
return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))
(mkApp (P Ref n ty) (map getP (reverse env'))))
where
mkTy [] t = t
@ -445,7 +447,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
ds = deferred ps in
ps { holes = hs \\ [x],
deferred = n : ds })
return (Bind n (GHole 0 fty)
return (Bind n (GHole 0 [] fty)
(mkApp (P Ref n ty) (map getP args)))
where
getP n = case lookup n env of

15
src/Idris/Core/TT.hs
View File

@ -809,6 +809,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
binderVal :: b }
| Hole { binderTy :: !b}
| GHole { envlen :: Int,
localnames :: [Name],
binderTy :: !b}
| Guess { binderTy :: !b,
binderVal :: b }
@ -827,7 +828,7 @@ instance Sized a => Sized (Binder a) where
size (Let ty val) = 1 + size ty + size val
size (NLet ty val) = 1 + size ty + size val
size (Hole ty) = 1 + size ty
size (GHole _ ty) = 1 + size ty
size (GHole _ _ ty) = 1 + size ty
size (Guess ty val) = 1 + size ty + size val
size (PVar ty) = 1 + size ty
size (PVTy ty) = 1 + size ty
@ -839,7 +840,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
fmapMB f (Lam t) = liftM Lam (f t)
fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)
fmapMB f (Hole t) = liftM Hole (f t)
fmapMB f (GHole i t) = liftM (GHole i) (f t)
fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)
fmapMB f (PVar t) = liftM PVar (f t)
fmapMB f (PVTy t) = liftM PVTy (f t)
@ -1494,7 +1495,7 @@ prettyEnv env t = prettyEnv' env t False
-- Render a `Binder` and its name
prettySb env n (Lam t) = prettyB env "λ" "=>" n t
prettySb env n (Hole t) = prettyB env "?defer" "." n t
prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t
prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t
prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t
prettySb env n (PVar t) = prettyB env "pat" "." n t
prettySb env n (PVTy t) = prettyB env "pty" "." n t
@ -1539,7 +1540,7 @@ showEnv' env t dbg = se 10 env t where
sb env n (Lam t) = showb env "\\ " " => " n t
sb env n (Hole t) = showb env "? " ". " n t
sb env n (GHole i t) = showb env "?defer " ". " n t
sb env n (GHole i ns t) = showb env "?defer " ". " n t
sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t
sb env n (Pi _ t _) = showb env "(" ") -> " n t
sb env n (PVar t) = showb env "pat " ". " n t
@ -1739,7 +1740,7 @@ pprintTT bound tm = pp startPrec bound tm
ppb p bound n (Hole ty) sc =
bracket p startPrec . group . align . hang 2 $
text "?" <+> bindingOf n False <+> text "." <> line <> sc
ppb p bound n (GHole _ ty) sc =
ppb p bound n (GHole _ _ ty) sc =
bracket p startPrec . group . align . hang 2 $
text "¿" <+> bindingOf n False <+> text "." <> line <> sc
ppb p bound n (Guess ty val) sc =
@ -1791,8 +1792,8 @@ pprintRaw bound (RBind n b body) =
vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]
ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $
text "Hole" <$> pprintRaw bound ty
ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $
text "GHole" <$> pprintRaw bound ty
ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $
text "GHole" <$> pprintRaw bound ty
ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $
vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]
ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

8
src/Idris/Core/Typecheck.hs
View File

@ -232,12 +232,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
let tt' = normalise ctxt env tt
lift $ isType ctxt env tt'
return (Hole tv, tt')
checkBinder (GHole i t)
checkBinder (GHole i ns t)
= do (tv, tt) <- chk u env t
let tv' = normalise ctxt env tv
let tt' = normalise ctxt env tt
lift $ isType ctxt env tt'
return (GHole i tv, tt')
return (GHole i ns tv, tt')
checkBinder (Guess t v)
| not holes = lift $ tfail (IncompleteTerm undefined)
| otherwise
@ -273,8 +273,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
= return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
discharge n (Hole t) bt scv sct
= return (Bind n (Hole t) scv, sct)
discharge n (GHole i t) bt scv sct
= return (Bind n (GHole i t) scv, sct)
discharge n (GHole i ns t) bt scv sct
= return (Bind n (GHole i ns t) scv, sct)
discharge n (Guess t v) bt scv sct
= return (Bind n (Guess t v) scv, sct)
discharge n (PVar t) bt scv sct

4
src/Idris/DeepSeq.hs
View File

@ -295,8 +295,8 @@ instance (NFData t) => NFData (PTactic' t) where
rnf Compute = ()
rnf Trivial = ()
rnf TCInstance = ()
rnf (ProofSearch r r1 r2 x1 x2)
= rnf x1 `seq` rnf x2 `seq` ()
rnf (ProofSearch r r1 r2 x1 x2 x3)
= rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
rnf Solve = ()
rnf Attack = ()
rnf ProofState = ()

4
src/Idris/Delaborate.hs
View File

@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
| Just n' <- lookup n env = PRef un [] n'
| otherwise
= case lookup n (idris_metavars ist) of
Just (Just _, mi, _) -> mkMVApp n []
Just (Just _, mi, _, _) -> mkMVApp n []
_ -> PRef un [] n
de env _ (Bind n (Lam ty) sc)
= PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)
@ -169,7 +169,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
= PApp un (de env [] f) (map pexp (map (de env []) args))
deFn env (P _ n _) args
| not mvs = case lookup n (idris_metavars ist) of
Just (Just _, mi, _) ->
Just (Just _, mi, _, _) ->
mkMVApp n (drop mi (map (de env []) args))
_ -> mkPApp n (map (de env []) args)
| otherwise = mkPApp n (map (de env []) args)

16
src/Idris/Elab/Clause.hs
View File

@ -632,6 +632,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
((rhs', defer, 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
mapM_ addPSname (allNamesIn lhs_in)
mapM_ setinj (nub (params ++ inj))
setNextName
(ElabResult _ _ is ctxt' newDecls highlights) <-
@ -656,9 +658,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
logLvl 5 "DONE CHECK"
logLvl 4 $ "---> " ++ show rhs'
when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++
show (map (\ (n, (_,_,t)) -> (n, t)) defer)
show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
def' <- checkDef fc (Elaborating "deferred type of ") defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
addDeferred def''
mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
@ -816,6 +818,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")
(bindTyArgs PVTy bargs infP) initEState
(do pbinds i lhs_tm
-- proof search can use explicitly written names
mapM_ addPSname (allNamesIn lhs_in)
setNextName
-- TODO: may want where here - see winfo abpve
(ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname
@ -828,7 +832,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
sendHighlighting highlights
def' <- checkDef fc iderr defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
addDeferred def''
mapM_ (elabCaseBlock info opts) is
logLvl 5 ("Checked wval " ++ show wval')
@ -890,8 +894,8 @@ 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))]
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
addDeferred def''
-- in the subdecls, lhs becomes:
@ -932,7 +936,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
sendHighlighting highlights
def' <- checkDef fc iderr defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
addDeferred def''
mapM_ (elabCaseBlock info opts) is
logLvl 5 ("Checked RHS " ++ show rhs')

36
src/Idris/Elab/Term.hs
View File

@ -41,7 +41,7 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS
data ElabResult =
ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
, resultMetavars :: [(Name, (Int, Maybe Name, Type))]
, resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
-- ^ Information about new metavariables
, resultCaseDecls :: [PDecl]
-- ^ Deferred declarations as the meaning of case blocks
@ -627,6 +627,7 @@ elab ist info emode opts fn tm
lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
checkPiGoal n
attack; intro (Just n);
addPSname n -- okay for proof search
-- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
elabE (ina { e_inarg = True } ) (Just fc) sc; solve
highlightSource nfc (AnnBoundName n False)
@ -643,6 +644,7 @@ elab ist info emode opts fn tm
ptm <- get_term
hs <- get_holes
introTy (Var tyn) (Just n)
addPSname n -- okay for proof search
focus tyn
elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
@ -651,6 +653,7 @@ elab ist info emode opts fn tm
highlightSource nfc (AnnBoundName n False)
elab' ina fc (PPi p n nfc Placeholder sc)
= do attack; arg n (is_scoped p) (sMN 0 "ty")
addPSname n -- okay for proof search
elabE (ina { e_inarg = True, e_intype = True }) fc sc
solve
highlightSource nfc (AnnBoundName n False)
@ -661,6 +664,7 @@ elab ist info emode opts fn tm
MN _ _ -> unique_hole n
_ -> return n
forall n' (is_scoped p) (Var tyn)
addPSname n' -- okay for proof search
focus tyn
let ec' = ina { e_inarg = True, e_intype = True }
elabE ec' fc ty
@ -676,6 +680,7 @@ elab ist info emode opts fn tm
claim valn (Var tyn)
explicit valn
letbind n (Var tyn) (Var valn)
addPSname n
case ty of
Placeholder -> return ()
_ -> do focus tyn
@ -961,6 +966,7 @@ elab ist info emode opts fn tm
let unique_used = getUniqueUsed (tt_ctxt ist) ptm
let n' = metavarName (namespace info) n
attack
psns <- getPSnames
defer unique_used n'
solve
highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
@ -1620,7 +1626,7 @@ solveAuto ist fn ambigok n
g <- goal
isg <- is_guess -- if it's a guess, we're working on it recursively, so stop
when (not isg) $
proofSearch' ist True ambigok 100 True Nothing fn []
proofSearch' ist True ambigok 100 True Nothing fn [] []
solveAutos :: IState -> Name -> Bool -> ElabD ()
solveAutos ist fn ambigok
@ -1629,12 +1635,12 @@ solveAutos ist fn ambigok
trivial' ist
= trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
trivialHoles' h ist
= trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
proofSearch' ist rec ambigok depth prv top n hints
trivialHoles' psn h ist
= trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
proofSearch' ist rec ambigok depth prv top n psns hints
= do unifyProblems
proofSearch rec prv ambigok (not prv) depth
(elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
(elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist
-- | Resolve type classes. This will only pick up 'normal' instances, never
-- named instances (which is enforced by 'findInstances').
@ -1674,7 +1680,7 @@ resTC' tcs defaultOn topholes depth topg fn ist
_ -> []
traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
try' (trivialHoles' okholes ist)
try' (trivialHoles' [] okholes ist)
(do addDefault t tc ttypes
let stk = map fst (filter snd $ elab_stack ist)
let insts = findInstances ist t
@ -1799,11 +1805,11 @@ resTC' tcs defaultOn topholes depth topg fn ist
isImp arg = (False, priority arg)
collectDeferred :: Maybe Name -> [Name] -> Context ->
Term -> State [(Name, (Int, Maybe Name, Type))] Term
collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =
do ds <- get
t' <- collectDeferred top casenames ctxt t
when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])
when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])
collectDeferred top casenames ctxt app
where
-- Evaluate the top level functions in arguments, if possible, and if it's
@ -2118,7 +2124,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
do actualHints <- mapM reifyTTName hs
unifyProblems
let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")
proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist
proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist
returnUnit
(Constant (I _), Nothing ) ->
lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
@ -2290,8 +2296,8 @@ runTac autoSolve ist perhapsFC fn tac
runT Compute = compute
runT Trivial = do trivial' ist; when autoSolve solveAll
runT TCInstance = runT (Exact (PResolveTC emptyFC))
runT (ProofSearch rec prover depth top hints)
= do proofSearch' ist rec False depth prover top fn hints
runT (ProofSearch rec prover depth top psns hints)
= do proofSearch' ist rec False depth prover top fn psns hints
when autoSolve solveAll
runT (Focus n) = focus n
runT Unfocus = do hs <- get_holes
@ -2499,7 +2505,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) [(n, (-1, Nothing, ty, []))]
addIBC (IBCDef n)
ctxt <- getContext
case lookupDef n ctxt of
@ -2508,7 +2514,7 @@ processTacticDecls info steps =
-- then it must be added as a metavariable. This needs guarding
-- to prevent overwriting case defs with a metavar, if the case
-- defs come after the type decl in the same script!
let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds
in addDeferred ds'
_ -> return ()
RAddInstance className instName ->

4
src/Idris/Elab/Type.hs
View File

@ -159,9 +159,9 @@ 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 [(n, (-1, Nothing, usety, []))]
addIBC (IBCDef n)
let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds
let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds
addDeferred ds'
setFlags n opts'
checkDocs fc argDocs ty

14
src/Idris/Elab/Utils.hs
View File

@ -40,21 +40,21 @@ recheckC_borrowing uniq_check bs fc mkerr env t
iderr :: Name -> Err -> Err
iderr _ e = e
checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]
-> Idris [(Name, (Int, Maybe Name, Type))]
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
checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
-> [(Name, (Int, Maybe Name, Type))]
-> Idris [(Name, (Int, Maybe Name, Type))]
-> [(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)) : ns)
checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)
= do ctxt <- getContext
(t', _) <- recheckC fc (mkerr n) [] t
when add $ do addDeferred [(n, (i, top, t, toplvl))]
when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]
addIBC (IBCDef n)
ns' <- checkAddDef add toplvl fc mkerr ns
return ((n, (i, top, t')) : ns')
return ((n, (i, top, t', psns)) : ns')
-- | Get the list of (index, name) of inaccessible arguments from an elaborated
-- type

2
src/Idris/Elab/Value.hs
View File

@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in
let vtm = orderPats (getInferTerm tm')
def' <- checkDef (fileFC "(input)") iderr defer
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) def'
addDeferred def''
mapM_ (elabCaseBlock info []) is

22
src/Idris/IBC.hs
View File

@ -40,7 +40,7 @@ import System.Directory
import Codec.Archive.Zip
ibcVersion :: Word16
ibcVersion = 116
ibcVersion = 117
data IBCFile = IBCFile { ver :: Word16,
sourcefile :: FilePath,
@ -78,7 +78,7 @@ data IBCFile = IBCFile { ver :: Word16,
ibc_metainformation :: ![(Name, MetaInformation)],
ibc_errorhandlers :: ![Name],
ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler
ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],
ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],
ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],
ibc_postulates :: ![Name],
ibc_externs :: ![(Name, Int)],
@ -610,7 +610,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()
pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->
addFunctionErrorHandlers fn arg [handler]) ns
pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()
pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris ()
pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })
----- For Cheapskate and docstrings
@ -1869,12 +1869,13 @@ instance (Binary t) => Binary (PTactic' t) where
put x1
ByReflection x1 -> do putWord8 20
put x1
ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21
put x1
put x2
put x3
put x4
put x5
ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21
put x1
put x2
put x3
put x4
put x5
put x6
DoUnify -> putWord8 22
CaseTac x1 -> do putWord8 23
put x1
@ -1954,7 +1955,8 @@ instance (Binary t) => Binary (PTactic' t) where
x3 <- get
x4 <- get
x5 <- get
return (ProofSearch x1 x2 x3 x4 x5)
x6 <- get
return (ProofSearch x1 x2 x3 x4 x5 x6)
22 -> return DoUnify
23 -> do x1 <- get
return (CaseTac x1)

4
src/Idris/IdrisDoc.hs
View File

@ -360,8 +360,8 @@ extractPTactic (MatchRefine n) = [n]
extractPTactic (LetTac n p) = n : extract p
extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]
extractPTactic (Exact p) = extract p
extractPTactic (ProofSearch _ _ _ m ns) | Just n <- m = n : ns
extractPTactic (ProofSearch _ _ _ _ ns) = ns
extractPTactic (ProofSearch _ _ _ m _ ns) | Just n <- m = n : ns
extractPTactic (ProofSearch _ _ _ _ _ ns) = ns
extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2]
extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2]
extractPTactic (ApplyTactic p) = extract p

13
src/Idris/Interactive.hs
View File

@ -213,12 +213,13 @@ doProofSearch fn updatefile rec l n hints (Just depth)
[] -> return n
ns -> ierror (CantResolveAlts ns)
i <- getIState
let (top, envlen, _) = case lookup mn (idris_metavars i) of
Just (t, e, False) -> (t, e, False)
_ -> (Nothing, 0, True)
let (top, envlen, psnames, _)
= case lookup mn (idris_metavars i) of
Just (t, e, ns, False) -> (t, e, ns, False)
_ -> (Nothing, 0, [], True)
let fc = fileFC fn
let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))
(ProofSearch rec False depth t hints)]
let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
(ProofSearch rec False depth t psnames hints)]
let def = PClause fc mn (PRef fc [] mn) [] (body top) []
newmv <- idrisCatch
(do elabDecl' EAll recinfo (PClauses fc [] mn [def])
@ -297,7 +298,7 @@ makeLemma fn updatefile l n
ns -> ierror (CantResolveAlts (map fst ns))
i <- getIState
margs <- case lookup n (idris_metavars i) of
Just (_, arity, _) -> return arity
Just (_, arity, _, _) -> return arity
_ -> return (-1)
if (not isProv) then do

4
src/Idris/ParseExpr.hs
View File

@ -971,7 +971,7 @@ autoImplicit opts st syn
sc <- expr syn
highlightP kw AnnKeyword
return (bindList (PPi
(TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)
(TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)
defaultImplicit opts st syn = do
kw <- reservedFC "default"
@ -1436,7 +1436,7 @@ tactics =
, noArgs ["unify"] DoUnify
, (["search"], Nothing, const $
do depth <- option 10 $ fst <$> natural
return (ProofSearch True True (fromInteger depth) Nothing []))
return (ProofSearch True True (fromInteger depth) Nothing [] []))
, noArgs ["instance"] TCInstance
, noArgs ["solve"] Solve
, noArgs ["attack"] Attack

20
src/Idris/ProofSearch.hs
View File

@ -22,10 +22,10 @@ import Debug.Trace
-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
trivial = trivialHoles []
trivial = trivialHoles [] []
trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles ok elab ist
trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles psnames ok elab ist
= try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])
return ())
(do env <- get_env
@ -41,7 +41,7 @@ trivialHoles ok elab ist
g <- goal
-- anywhere but the top is okay for a hole, if holesOK set
if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
holesOK hs (binderTy b)
holesOK hs (binderTy b) && (null psnames || x `elem` psnames)
then try' (elab (PRef (fileFC "prf") [] x))
(tryAll xs) True
else tryAll xs
@ -73,9 +73,11 @@ proofSearch :: Bool -> -- recursive search (False for 'refine')
Bool -> -- ambiguity ok
Bool -> -- defer on failure
Int -> -- maximum depth
(PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
(PTerm -> ElabD ()) -> Maybe Name -> Name ->
[Name] ->
[Name] ->
IState -> ElabD ()
proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist
= do -- get all possible versions of the name, take the first one that
-- works
let all_imps = lookupCtxtName fn (idris_implicits ist)
@ -106,7 +108,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
isImp (PImp p _ _ _ _) = (True, p)
isImp arg = (True, priority arg) -- try to get all of them by unification
proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
= do compute
ty <- goal
hs <- get_holes
@ -177,7 +179,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
ty <- goal
when (S.member ty tys) $ fail "Been here before"
let tys' = S.insert ty tys
try' (trivial elab ist)
try' (trivialHoles psnames [] elab ist)
(try' (try' (resolveByCon (d - 1) locs tys')
(resolveByLocals (d - 1) locs tys')
True)
@ -215,7 +217,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
tryLocals d locs tys [] = fail "Locals failed"
tryLocals d locs tys ((x, t) : xs)
| x `elem` locs = tryLocals d locs tys xs
| x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
| otherwise = try' (tryLocal d (x : locs) tys x t)
(tryLocals d locs tys xs) True

10
src/Idris/REPL.hs
View File

@ -904,8 +904,8 @@ process fn (Check (PRef _ _ n))
case lookupNames n ctxt of
ts@(t:_) ->
case lookup t (idris_metavars ist) of
Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
showMetavarInfo ppo ist n i
Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
showMetavarInfo ppo ist n i
Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
[] -> iPrintError $ "No such variable " ++ show n
where
@ -1079,7 +1079,7 @@ process fn (RmProof n')
insertMetavar n =
do i <- getIState
let ms = idris_metavars i
putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
putIState $ i { idris_metavars = (n, (Nothing, 0, [], False)) : ms }
process fn' (AddProof prf)
= do fn <- do
@ -1132,8 +1132,8 @@ process fn (Prove mode n')
let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
n <- case metavars of
[] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
[(n, (_,_,False))] -> return n
[(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
[(n, (_,_,_,False))] -> return n
[(_, (_,_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
ns -> ierror (CantResolveAlts (map fst ns))
prover mode (lit fn) n
-- recheck totality

8
src/Idris/Reflection.hs
View File

@ -76,7 +76,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)
reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
reifyApp _ t [Constant (I i)]
| t == reflm "Search" = return (ProofSearch True True i Nothing [])
| t == reflm "Search" = return (ProofSearch True True i Nothing [] [])
reifyApp _ t [x]
| t == reflm "Refine" = do n <- reifyTTName x
return $ Refine n []
@ -307,7 +307,7 @@ reifyTTBinderApp reif f [x, y]
reifyTTBinderApp reif f [t]
| f == reflm "Hole" = liftM Hole (reif t)
reifyTTBinderApp reif f [t]
| f == reflm "GHole" = liftM (GHole 0) (reif t)
| f == reflm "GHole" = liftM (GHole 0 []) (reif t)
reifyTTBinderApp reif f [x, y]
| f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
reifyTTBinderApp reif f [t]
@ -580,7 +580,7 @@ reflectBinderQuotePattern q ty unq (Hole t)
fill $ reflCall "Hole" [ty, Var t']
solve
focus t'; q unq t
reflectBinderQuotePattern q ty unq (GHole _ t)
reflectBinderQuotePattern q ty unq (GHole _ _ t)
= do t' <- claimTy (sMN 0 "ty") ty; movelast t'
fill $ reflCall "GHole" [ty, Var t']
solve
@ -731,7 +731,7 @@ reflectBinderQuote q ty unq (NLet x y)
= reflCall "NLet" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (Hole t)
= reflCall "Hole" [Var ty, q unq t]
reflectBinderQuote q ty unq (GHole _ t)
reflectBinderQuote q ty unq (GHole _ _ t)
= reflCall "GHole" [Var ty, q unq t]
reflectBinderQuote q ty unq (Guess x y)
= reflCall "Guess" [Var ty, q unq x, q unq y]

1
test/interactive003/expected
View File

@ -2,3 +2,4 @@ ys
x :: app xs ys
[]
f x y :: vzipWith f xs ys
?word_length_rhs_3 :: word_length xs

1
test/interactive003/input
View File

@ -2,3 +2,4 @@
:ps 5 app_rhs_2
:ps 8 vzipWith_rhs_3
:ps 9 vzipWith_rhs_1
:ps 13 word_length_rhs_2

5
test/interactive003/interactive003.idr
View File

@ -8,3 +8,8 @@ vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_3
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1
word_length : Vect n String -> Vect n Nat
word_length [] = []
word_length (x :: xs) = ?word_length_rhs_2