edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 18:53:42 +03:00
Code Issues Projects Releases Wiki Activity

Record whether a definition originated from a hole

Browse Source
This commit is contained in:
Edwin Brady 2020-02-22 15:04:35 +00:00
parent f2a1934508
commit 3bb5002dba
8 changed files with 65 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 14
ttcVersion = 15
export
checkTTCVersion : Int -> Int -> Core ()

22
src/Core/Context.idr
View File

@ -20,10 +20,25 @@ import System
%default covering
public export
data HoleInfo
= NotHole
| SolvedHole Nat
public export
record PMDefInfo where
constructor MkPMDefInfo
holeInfo : HoleInfo
alwaysReduce : Bool
export
defaultPI : PMDefInfo
defaultPI = MkPMDefInfo NotHole False
public export
data Def : Type where
None : Def -- Not yet defined
PMDef : (alwaysReduce : Bool) -> -- always reduce, even when quoting etc
PMDef : (pminfo : PMDefInfo) -> -- always reduce, even when quoting etc
-- typically for inlinable metavariable solutions
(args : List Name) ->
(treeCT : CaseTree args) ->
@ -336,7 +351,10 @@ returnDef : Bool -> Int -> GlobalDef -> Maybe (Int, GlobalDef)
returnDef False idx def = Just (idx, def)
returnDef True idx def
= case definition def of
PMDef True _ _ _ _ => Just (idx, def)
PMDef pi _ _ _ _ =>
if alwaysReduce pi
then Just (idx, def)
else Nothing
_ => Nothing
export

2
src/Core/Normalise.idr
View File

@ -373,7 +373,7 @@ parameters (defs : Defs, topopts : EvalOpts)
-- + It's a metavariable and not in Rig0
-- + It's a metavariable and we're not in 'argHolesOnly'
-- + It's inlinable and we're in 'tcInline'
= if r
= if alwaysReduce r
|| (not (holesOnly opts) && not (argHolesOnly opts) && not (tcInline opts))
|| (meta && rigd /= Rig0)
|| (meta && holesOnly opts)

29
src/Core/TTC.idr
View File

@ -747,12 +747,32 @@ TTC PrimNames where
c <- fromBuf b
pure (MkPrimNs i str c)
export
TTC HoleInfo where
toBuf b NotHole = tag 0
toBuf b (SolvedHole n) = do tag 1; toBuf b n
fromBuf b
= case !getTag of
0 => pure NotHole
1 => do n <- fromBuf b; pure (SolvedHole n)
_ => corrupt "HoleInfo"
export
TTC PMDefInfo where
toBuf b l
= do toBuf b (holeInfo l)
toBuf b (alwaysReduce l)
fromBuf b
= do h <- fromBuf b
r <- fromBuf b
pure (MkPMDefInfo h r)
export
TTC Def where
toBuf b None = tag 0
toBuf b (PMDef r args ct rt pats)
= do tag 1; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats
toBuf b (PMDef pi args ct rt pats)
= do tag 1; toBuf b pi; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats
toBuf b (ExternDef a)
= do tag 2; toBuf b a
toBuf b (ForeignDef a cs)
@ -776,11 +796,12 @@ TTC Def where
fromBuf b
= case !getTag of
0 => pure None
1 => do args <- fromBuf b
1 => do pi <- fromBuf b
args <- fromBuf b
ct <- fromBuf b
rt <- fromBuf b
pats <- fromBuf b
pure (PMDef False args ct rt pats)
pure (PMDef pi args ct rt pats)
2 => do a <- fromBuf b
pure (ExternDef a)
3 => do a <- fromBuf b

19
src/Core/Unify.idr
View File

@ -316,12 +316,13 @@ instantiate : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{newvars : _} ->
FC -> UnifyMode -> Env Term vars ->
(metavar : Name) -> (mref : Int) -> (mdef : GlobalDef) ->
(metavar : Name) -> (mref : Int) -> (numargs : Nat) ->
(mdef : GlobalDef) ->
List (Var newvars) -> -- Variable each argument maps to
Term vars -> -- original, just for error message
Term newvars -> -- shrunk environment
Core ()
instantiate {newvars} loc mode env mname mref mdef locs otm tm
instantiate {newvars} loc mode env mname mref num mdef locs otm tm
= do logTerm 5 ("Instantiating in " ++ show newvars) tm
-- let Hole _ _ = definition mdef
-- | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
@ -339,7 +340,7 @@ instantiate {newvars} loc mode env mname mref mdef locs otm tm
logTerm 5 ("Instantiated: " ++ show mname) ty
log 5 ("From vars: " ++ show newvars)
logTerm 5 "Definition" rhs
let simpleDef = isSimple rhs
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
let newdef = record { definition =
PMDef simpleDef [] (STerm rhs) (STerm rhs) []
} mdef
@ -430,7 +431,7 @@ solveIfUndefined env (Meta fc mname idx args) soln
Just stm =>
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (InternalError "Can't happen: no definition")
instantiate fc (InTerm True) env mname idx hdef locs soln stm
instantiate fc (InTerm True) env mname idx (length args) hdef locs soln stm
pure True
solveIfUndefined env metavar soln
= pure False
@ -628,7 +629,7 @@ mutual
-- metavariables)
do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
| Nothing => throw (InternalError ("Can't happen: Lost hole " ++ show mname))
instantiate loc mode env mname mref hdef locs solfull stm
instantiate loc mode env mname mref (length margs) hdef locs solfull stm
pure $ solvedHole mref
where
-- Only need to check the head metavar is the same, we've already
@ -1160,7 +1161,7 @@ retryGuess mode smode (hid, (loc, hname))
handleUnify
(do tm <- search loc rig (smode == Defaults) depth defining
(type def) []
let gdef = record { definition = PMDef False [] (STerm tm) (STerm tm) [] } def
let gdef = record { definition = PMDef defaultPI [] (STerm tm) (STerm tm) [] } def
logTermNF 5 ("Solved " ++ show hname) [] tm
addDef (Resolved hid) gdef
removeGuess hid
@ -1189,7 +1190,8 @@ retryGuess mode smode (hid, (loc, hname))
AddDelay r =>
do ty <- getType [] tm
pure $ delayMeta r envb !(getTerm ty) tm
let gdef = record { definition = PMDef True [] (STerm tm') (STerm tm') [] } def
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] (STerm tm') (STerm tm') [] } def
logTerm 5 ("Resolved " ++ show hname) tm'
addDef (Resolved hid) gdef
removeGuess hid
@ -1207,7 +1209,8 @@ retryGuess mode smode (hid, (loc, hname))
-- All constraints resolved, so turn into a
-- proper definition and remove it from the
-- hole list
[] => do let gdef = record { definition = PMDef True [] (STerm tm) (STerm tm) [] } def
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] (STerm tm) (STerm tm) [] } def
logTerm 5 ("Resolved " ++ show hname) tm
addDef (Resolved hid) gdef
removeGuess hid

7
src/Idris/REPL.idr
View File

@ -70,6 +70,10 @@ isHole : GlobalDef -> Maybe Nat
isHole def
= case definition def of
Hole locs _ => Just locs
PMDef pi _ _ _ _ =>
case holeInfo pi of
NotHole => Nothing
SolvedHole n => Just n
_ => Nothing
showCount : RigCount -> String
@ -362,8 +366,7 @@ processEdit (ExprSearch upd line name hints all)
else x) in
if upd
then updateFile (proofSearch name res (cast (line - 1)))
else pure $ DisplayEdit
[res ]
else pure $ DisplayEdit [res]
[] => pure $ EditError $ "Unknown name " ++ show name
_ => pure $ EditError "Not a searchable hole"
where

2
src/TTImp/Elab/Delayed.idr
View File

@ -129,7 +129,7 @@ retryDelayed ((i, elab) :: ds)
log 5 ("Retrying delayed hole " ++ show !(getFullName (Resolved i)))
tm <- elab
updateDef (Resolved i) (const (Just
(PMDef True [] (STerm tm) (STerm tm) [])))
(PMDef (MkPMDefInfo NotHole True) [] (STerm tm) (STerm tm) [])))
logTerm 5 ("Resolved delayed hole " ++ show i) tm
logTermNF 5 ("Resolved delayed hole NF " ++ show i) [] tm
removeHole i

2
src/TTImp/ProcessDef.idr
View File

@ -612,7 +612,7 @@ processDef opts nest env fc n_in cs_in
-- but we'll rebuild that in a later pass once all the case
-- blocks etc are resolved
addDef (Resolved nidx)
(record { definition = PMDef False cargs tree_ct tree_ct pats
(record { definition = PMDef defaultPI cargs tree_ct tree_ct pats
} gdef)
let rmetas = getMetas tree_ct