From a7bf075c945530d2c6657af0c4528dd47ceb815a Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 15 Jun 2019 12:42:35 +0100 Subject: [PATCH] Get GlobalHint flag right 'True' means a default hint, which is only used if all else fails (and is only really intended to get default Integer) --- libs/base/Control/WellFounded.idr | 2 +- src/Core/AutoSearch.idr | 7 +++-- src/Core/Context.idr | 4 +-- src/Core/Unify.idr | 43 +++++++++++++++++-------------- src/Idris/Parser.idr | 7 +++-- src/Idris/REPL.idr | 4 +++ src/Idris/Syntax.idr | 1 + src/TTImp/TTImp.idr | 3 +-- 8 files changed, 43 insertions(+), 28 deletions(-) diff --git a/libs/base/Control/WellFounded.idr b/libs/base/Control/WellFounded.idr index 886b3b0..488bae4 100644 --- a/libs/base/Control/WellFounded.idr +++ b/libs/base/Control/WellFounded.idr @@ -40,7 +40,7 @@ Smaller x y = size x `LT` size y SizeAccessible : Sized a => a -> Type SizeAccessible = Accessible Smaller - + sizeAccessible : Sized a => (x : a) -> SizeAccessible x sizeAccessible x = Access (acc $ size x) where diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index 0925049..58016fd 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -412,7 +412,9 @@ searchType {vars} fc rigc defaults depth def top env target tryGroups nty [] = throw (CantSolveGoal fc [] top) tryGroups nty (g :: gs) = handleUnify - (searchNames fc rigc defaults depth def top env g nty) + (do logC 5 (do gn <- traverse getFullName g + pure ("Search: Trying names " ++ show gn)) + searchNames fc rigc defaults depth def top env g nty) (\err => if ambig err || isNil gs then throw err else tryGroups nty gs) @@ -427,7 +429,8 @@ searchType {vars} fc rigc defaults depth def top env target Core.Unify.search fc rigc defaults depth def top_in env = do defs <- get Ctxt top <- normaliseScope defs env top_in - logTerm 10 "Initial target: " top + logTerm 2 "Initial target: " top + log 2 $ "Running search with defaults " ++ show defaults tm <- searchType fc rigc defaults depth def (abstractEnvType fc env top) env top diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 7221d0f..0aad634 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -945,9 +945,9 @@ getSearchData fc defaults target Just hs => hs Nothing => [] if defaults - then let defaults = map fst (filter isDefault + then let defns = map fst (filter isDefault (toList (autoHints defs))) in - pure (MkSearchData [] [defaults]) + pure (MkSearchData [] [defns]) else let opens = map fst (toList (openHints defs)) autos = map fst (filter (not . isDefault) (toList (autoHints defs))) diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 6bf7839..92c10a7 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -1013,25 +1013,30 @@ retryGuess mode smode (hid, (loc, hname)) Just def => case definition def of BySearch rig depth defining => - handleUnify - (do tm <- search loc rig (smode == Defaults) depth defining - (type def) [] - let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def - logTerm 5 ("Solved " ++ show hname) tm - addDef (Resolved hid) gdef - removeGuess hid - pure True) - (\err => case err of - DeterminingArg _ n i _ _ => - do logTerm 5 ("Failed (det " ++ show hname ++ ")") - (type def) - setInvertible loc i - pure False -- progress made! - _ => do logTerm 5 ("Search failed for " ++ show hname) - (type def) - case smode of - LastChance => throw err - _ => pure False) -- Postpone again + case smode of + LastChance => + do log 5 $ "Last chance at " ++ show hname + search loc rig False depth defining (type def) [] + pure True + _ => handleUnify + (do tm <- search loc rig (smode == Defaults) depth defining + (type def) [] + let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def + logTerm 5 ("Solved " ++ show hname) tm + addDef (Resolved hid) gdef + removeGuess hid + pure True) + (\err => case err of + DeterminingArg _ n i _ _ => + do logTerm 5 ("Failed (det " ++ show hname ++ ")") + (type def) + setInvertible loc i + pure False -- progress made! + _ => do logTerm 5 ("Search failed for " ++ show hname) + (type def) + case smode of + LastChance => throw err + _ => pure False) -- Postpone again Guess tm constrs => do cs' <- traverse (retry mode) constrs let csAll = unionAll cs' diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 0b16aab..43fd43a 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -968,9 +968,9 @@ fnDirectOpt = do exactIdent "hint" pure (Hint True) <|> do exactIdent "globalhint" - pure (GlobalHint True) - <|> do exactIdent "defaulthint" pure (GlobalHint False) + <|> do exactIdent "defaulthint" + pure (GlobalHint True) <|> do exactIdent "inline" pure Inline <|> do exactIdent "extern" @@ -1381,6 +1381,9 @@ command <|> do symbol ":"; keyword "total" n <- name pure (Total n) + <|> do symbol ":"; replCmd ["log", "logging"] + i <- intLit + pure (SetLog (fromInteger i)) <|> do symbol ":"; cmd <- editCmd pure (Editing cmd) <|> do tm <- expr EqOK "(interactive)" init diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 8edb433..a768fdf 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -521,6 +521,10 @@ process (DebugInfo n) process (SetOpt opt) = do setOpt opt pure True +process (SetLog lvl) + = do setLogLevel lvl + iputStrLn $ "Log level to set " ++ show lvl + pure True process (Editing cmd) = do ppopts <- getPPrint -- Since we're working in a local environment, don't do the usual diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 6bc7575..efabbee 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -271,6 +271,7 @@ data REPLCmd : Type where CD : String -> REPLCmd Missing : Name -> REPLCmd Total : Name -> REPLCmd + SetLog : Nat -> REPLCmd Editing : EditCmd -> REPLCmd Quit : REPLCmd diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index ab2edfd..8137534 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -156,8 +156,7 @@ mutual -- Flag means the hint is a direct hint, not a function which might -- find the result (e.g. chasing parent interface dictionaries) Hint : Bool -> FnOpt - -- flag means always use this in search. If not set, it is only - -- used as a hint if all else fails (i.e. a default) + -- Flag means to use as a default if all else fails GlobalHint : Bool -> FnOpt ExternFn : FnOpt -- assume safe to cancel arguments in unification