Fix expression search on already solved holes

If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
This commit is contained in:
Edwin Brady 2021-06-23 00:59:26 +01:00
parent 92066c24fe
commit 4ef29da87e
11 changed files with 88 additions and 2 deletions

View File

@ -451,7 +451,7 @@ processEdit (ExprSearch upd line name hints)
case holeInfo pi of
NotHole => pure $ EditError "Not a searchable hole"
SolvedHole locs =>
do let (_ ** (env, tm')) = dropLamsTm locs [] tm
do let (_ ** (env, tm')) = dropLamsTm locs [] !(normaliseHoles defs [] tm)
itm <- resugar env tm'
let itm' : PTerm = if brack then addBracket replFC itm else itm
if upd

View File

@ -888,6 +888,13 @@ exprSearchOpts opts fc n_in hints
= do defs <- get Ctxt
Just (n, idx, gdef) <- lookupHoleName n_in defs
| Nothing => undefinedName fc n_in
-- the REPL does this step, but doing it here too because
-- expression search might be invoked some other way
let Hole _ _ = definition gdef
| PMDef pi [] (STerm _ tm) _ _
=> do raw <- unelab [] !(toFullNames !(normaliseHoles defs [] tm))
one raw
| _ => throw (GenericMsg fc "Name is already defined")
lhs <- findHoleLHS !(getFullName (Resolved idx))
log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs)
opts' <- if getRecData opts

View File

@ -79,7 +79,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
"interactive021", "interactive022", "interactive023", "interactive024",
"interactive025", "interactive026", "interactive027", "interactive028",
"interactive029", "interactive030", "interactive031", "interactive032",
"interactive033", "interactive034"]
"interactive033", "interactive034", "interactive035"]
idrisTestsInterface : TestPool
idrisTestsInterface = MkTestPool "Interface" [] Nothing

View File

@ -0,0 +1,3 @@
1/1: Building timeout (timeout.idr)
Main> tailIsNotSound contra (ConsIsSound headIsSound tailIsSound) = contra tailIsSound
Main> Bye for now!

View File

@ -0,0 +1,2 @@
:gd 54 tailIsNotSound
:q

View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner timeout.idr < input
rm -rf build

View File

@ -0,0 +1,56 @@
import Data.List
import Data.List.Elem
%search_timeout 1000
||| A Place has an ID and a number of tokens
data Place : Type where
MkPlace : (i : Nat) -> (nTokens : Nat) -> Place
||| A transition has a name
data Transition : Type where
MkTransition : String -> Transition
||| An Input links a Place and a Transition...
data Input : Type where
MkInput : (from : Place) -> (to : Transition) -> Input
-- Accessor functions for proof
0 inputFrom : Input -> Place
inputFrom (MkInput p t) = p
0 inputTo : Input -> Transition
inputTo (MkInput p t) = t
data SoundInputFrom : Input -> List Place -> Type where
MkSoundInputFrom : (i : Input)
-> (ps : List Place)
-> (prf : Elem (inputFrom i) ps)
-> SoundInputFrom i ps
data SoundInputTo : Input -> List Transition -> Type where
MkSoundInputTo : (i : Input)
-> (ts : List Transition)
-> (prf : Elem (inputTo i) ts)
-> SoundInputTo i ts
data SoundInput : Input -> List Place -> List Transition -> Type where
MkSoundInput : (i : Input)
-> (ps : List Place)
-> (ts : List Transition)
-> (fromOK : SoundInputFrom i ps)
-> (toOK : SoundInputTo i ts)
-> SoundInput i ps ts
data AllInputsSound : List Input -> List Place -> List Transition -> Type where
NilInputsIsSound : AllInputsSound [] _ _
ConsIsSound : (headIsSound : SoundInput i ps ts)
-> (tailIsSound : AllInputsSound is ps ts)
-> AllInputsSound (i :: is) ps ts
-- Searching here finds the right answer immediately, but then if we don't
-- have a timeout, it takes ages to explore more non-solutions! So we cut off
-- after a second
tailIsNotSound : (contra : (AllInputsSound is ps ts -> Void))
-> AllInputsSound (i :: is) ps ts
-> Void

View File

@ -0,0 +1,3 @@
1/1: Building unify (unify.idr)
Main> 4
Main> Bye for now!

View File

@ -0,0 +1,2 @@
:ps 7 vlength
:q

View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner unify.idr < input
rm -rf build

View File

@ -0,0 +1,7 @@
import Data.Vect
data VectN : Type -> Type where
MkVectN : (n : Nat) -> Vect n a -> VectN a
doSearch : Nat -> VectN Int
doSearch n = MkVectN ?vlength [1,2,3,4]