dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

Keep track of autos to be solved, shaves about 12% off of Elab.newt processing time

Browse Source
This commit is contained in:
Steve Dunham
2025-04-05 21:25:53 -07:00
parent 549cca19e3
commit eeb790f1b2
10 changed files with 134 additions and 90 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Lib/CompileExp.newt
View File

@@ -110,7 +110,7 @@ compileTerm t@(Ref fc nm@(QN _ tag)) = do
_ => pure $ CRef nm
_ => apply (CRef nm) Nil Lin arity
compileTerm (Meta _ k) = pure $ CRef (QN Nil "meta$\{show k}") -- FIXME should be exception
compileTerm (Meta fc k) = error fc "Compiling meta \{show k}"
compileTerm (Lam _ nm _ _ t) = CLam nm <$> compileTerm t
compileTerm tm@(App _ _ _) = case funArgs tm of
(Meta _ k, args) => do

36
src/Lib/Elab.newt
View File

@@ -114,10 +114,9 @@ isCandidate (VRef _ nm _) (Ref fc nm') = nm == nm'
isCandidate ty (App fc t u) = isCandidate ty t
isCandidate _ _ = False
findMatches : Context -> Val -> List TopEntry -> M (List String)
findMatches : Context -> Val -> List (QName × Tm) -> M (List String)
findMatches ctx ty Nil = pure Nil
findMatches ctx ty ((MkEntry _ name type def flags) :: xs) = do
let (True) = elem Hint flags | False => findMatches ctx ty xs
findMatches ctx ty ((name, type) :: xs) = do
let (True) = isCandidate ty type
| False => findMatches ctx ty xs
@@ -130,7 +129,7 @@ findMatches ctx ty ((MkEntry _ name type def flags) :: xs) = do
-- This check is solving metas, so we save mc below in case we want this solution
let (QN ns nm) = name
let (cod, tele) = splitTele type
modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.autos mc.next CheckFirst
tm <- check ctx (RVar fc nm) ty
debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
writeIORef top.metaCtx mc
@@ -195,11 +194,10 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
| res => do
debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
pure False
let te = listValues top.defs
let rest = map {List} (\ x => listValues x.modDefs) $
mapMaybe (flip lookupMap' top.modules) top.imported
(nm :: Nil) <- findMatches ctx ty $ join (te :: rest)
let (VRef _ tyname _) = ty | _ => pure False
let cands = fromMaybe Nil $ lookupMap' tyname top.hints
(nm :: Nil) <- findMatches ctx ty cands
| res => do
debug $ \ _ => "FAILED to solve \{show ty}, matches: \{show res}"
pure False
@@ -215,7 +213,8 @@ solveAutos : M Unit
solveAutos = do
top <- getTop
mc <- readIORef top.metaCtx
res <- run $ filter isAuto (listValues mc.metas)
let autos = filter isAuto $ mapMaybe (flip lookupMap' mc.metas) mc.autos
res <- run autos
if res then solveAutos else pure MkUnit
where
isAuto : MetaEntry -> Bool
@@ -236,7 +235,10 @@ updateMeta ix f = do
mc <- readIORef {M} top.metaCtx
let (Just me) = lookupMap' ix mc.metas | Nothing => pure MkUnit
me <- f me
writeIORef top.metaCtx $ MC (updateMap ix me mc.metas) mc.next mc.mcmode
let autos = case me of
Solved _ _ _ => filter (_/=_ ix) mc.autos
_ => mc.autos
writeIORef top.metaCtx $ MC (updateMap ix me mc.metas) autos mc.next mc.mcmode
checkAutos : QName -> List MetaEntry -> M Unit
checkAutos ix Nil = pure MkUnit
@@ -263,8 +265,7 @@ addConstraint env ix sp tm = do
(Solved _ k tm) => error' "Meta \{show k} already solved [addConstraint]"
(OutOfScope) => error' "Meta \{show ix} out of scope"
mc <- readIORef top.metaCtx
checkAutos ix (listValues mc.metas)
pure MkUnit
checkAutos ix $ mapMaybe (flip lookupMap' mc.metas) mc.autos
-- return renaming, the position is the new VVar
invert : Int -> SnocList Val -> M (List Int)
@@ -353,9 +354,9 @@ maybeCheck action = do
case mc.mcmode of
CheckAll => action
CheckFirst => do
modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next NoCheck
modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.autos mc.next NoCheck
action
modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.autos mc.next CheckFirst
NoCheck => pure MkUnit
solve env m sp t = do
@@ -393,8 +394,6 @@ solve env m sp t = do
debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}"
unify env UNormal val rhs
mc <- readIORef top.metaCtx
-- stack ...
-- checkAutos ix mc.metas
pure MkUnit
)
@@ -587,7 +586,10 @@ freshMeta ctx fc ty kind = do
-- we were fudging this for v1
let qn = QN top.ns "$m\{show mc.next}"
let newmeta = Unsolved fc qn ctx ty kind Nil
writeIORef top.metaCtx $ MC (updateMap qn newmeta mc.metas) (1 + mc.next) mc.mcmode
let autos = case kind of
AutoSolve => qn :: mc.autos
_ => mc.autos
writeIORef top.metaCtx $ MC (updateMap qn newmeta mc.metas) autos (1 + mc.next) mc.mcmode
-- infinite loop - keeps trying Ord a => Ord (a \x a)
-- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta
pure $ applyBDs 0 (Meta fc qn) ctx.bds

24
src/Lib/ProcessDecl.newt
View File

@@ -51,9 +51,7 @@ logMetas (Unsolved fc k ctx ty User cons :: rest) = do
logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
ty' <- forceMeta ty
tm <- quote ctx.lvl ty'
-- Now that we're collecting errors, maybe we simply check at the end
-- TODO - log constraints?
-- FIXME in Combinatory, the val doesn't match environment?
-- FIXME in Combinatory.newt, the val doesn't match environment?
let msg = "Unsolved meta \{show k} \{show kind} type \{render 90 $ pprint (names ctx) tm} \{show $ length' cons} constraints"
msgs <- for cons $ \case
(MkMc fc env sp val) => do
@@ -65,13 +63,10 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
debug $ \ _ => "AUTO ---> \{show ty}"
-- we want the context here too.
top <- getTop
-- matches <- case !(contextMatches ctx ty) of
-- Nil => findMatches ctx ty $ toList top.defs
-- xs => pure xs
matches <- findMatches ctx ty $ map snd $ toList top.defs
-- TODO try putting mc into TopContext for to see if it gives better terms
let (VRef _ tyname _) = ty | _ => pure Nil
let cands = fromMaybe Nil $ lookupMap' tyname top.hints
matches <- findMatches ctx ty cands
pure $ (" \{show $ length' matches} Solutions: \{show matches}" :: Nil)
-- pure $ " \{show $ length' matches} Solutions:" :: map ((" " ++) ∘ render 90 ∘ pprint (names ctx) ∘ fst) matches
_ => pure Nil
info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
@@ -162,9 +157,7 @@ processDef ns fc nm clauses = do
-- I can take LHS apart syntactically or elaborate it with an infer
clauses' <- traverse makeClause clauses
tm <- buildTree (mkCtx fc) (MkProb clauses' vty)
-- log 1 $ \ _ => "Ok \{render 90 $ pprint Nil tm}"
mc <- readIORef top.metaCtx
solveAutos
-- TODO - make nf that expands all metas and drop zonk
-- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure.
@@ -267,10 +260,11 @@ processInstance ns instfc ty decls = do
-- member
case lookupRaw instname top of
Just _ => pure MkUnit -- TODO check that the types match
Nothing => processDecl ns sigDecl
setFlag (QN ns instname) instfc Hint
-- TODO add to hint dictionary
Nothing => do
-- only add once
processDecl ns sigDecl
setFlag (QN ns instname) instfc Hint
addHint (QN ns instname)
let (Just decls) = collectDecl <$> decls
| _ => do

42
src/Lib/TopContext.newt
View File

@@ -37,14 +37,14 @@ lookupRaw raw top =
instance Show TopContext where
show (MkTop _ _ _ defs metas _ _ _) = "\nContext:\n (\{ joinBy "\n" $ map (show ∘ snd) $ toList defs} :: Nil)"
show (MkTop _ _ _ _ defs metas _ _ _) = "\nContext:\n (\{ joinBy "\n" $ map (show ∘ snd) $ toList defs} :: Nil)"
-- TODO need to get class dependencies working
emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
emptyTop = do
mcctx <- newIORef (MC EmptyMap 0 CheckAll)
mcctx <- newIORef (MC EmptyMap Nil 0 CheckAll)
errs <- newIORef $ the (List Error) Nil
pure $ MkTop EmptyMap Nil Nil EmptyMap mcctx 0 errs EmptyMap
pure $ MkTop EmptyMap Nil EmptyMap Nil EmptyMap mcctx 0 errs EmptyMap
setFlag : QName → FC → EFlag → M Unit
@@ -53,9 +53,9 @@ setFlag name fc flag = do
let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.defs
| Nothing => error fc "\{show name} not declared"
modifyTop $ \case
MkTop mods imp ns defs metaCtx verbose errors ops =>
MkTop mods imp hints ns defs metaCtx verbose errors ops =>
let defs = (updateMap name (MkEntry fc name ty def (flag :: flags)) defs) in
MkTop mods imp ns defs metaCtx verbose errors ops
MkTop mods imp hints ns defs metaCtx verbose errors ops
setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
setDef name fc ty def flags = do
@@ -63,9 +63,9 @@ setDef name fc ty def flags = do
let (Nothing) = lookupMap' name top.defs
| Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}"
modifyTop $ \case
MkTop mods imp ns defs metaCtx verbose errors ops =>
MkTop mods imp hints ns defs metaCtx verbose errors ops =>
let defs = (updateMap name (MkEntry fc name ty def flags) top.defs) in
MkTop mods imp ns defs metaCtx verbose errors ops
MkTop mods imp hints ns defs metaCtx verbose errors ops
updateDef : QName -> FC -> Tm -> Def -> M Unit
@@ -74,9 +74,33 @@ updateDef name fc ty def = do
let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.defs
| Nothing => error fc "\{show name} not declared"
modifyTop $ \case
MkTop mods imp ns defs metaCtx verbose errors ops =>
MkTop mods imp hints ns defs metaCtx verbose errors ops =>
let defs = (updateMap name (MkEntry fc' name ty def flags) defs) in
MkTop mods imp ns defs metaCtx verbose errors ops
MkTop mods imp hints ns defs metaCtx verbose errors ops
typeName : Tm → Maybe QName
typeName (Pi fc nm Explicit rig t u) = Nothing
typeName (Pi fc name icit rig t u) = typeName u
typeName (App fc t u) = typeName t
typeName (Ref _ nm) = Just nm
typeName _ = Nothing
addHint : QName → M Unit
addHint qn = do
top <- getTop
case lookup qn top of
Just entry => do
let (Just tyname) = typeName entry.type
| Nothing => error entry.fc "can't find tcon name for \{show qn}"
let xs = fromMaybe Nil $ lookupMap' tyname top.hints
let hints = updateMap tyname ((qn, entry.type) :: xs) top.hints
putTop $ MkTop top.modules top.imported hints top.ns top.defs top.metaCtx top.verbose top.errors top.ops
pure MkUnit
Nothing => pure MkUnit
addError : Error -> M Unit
addError err = do

8
src/Lib/Types.newt
View File

@@ -304,6 +304,7 @@ data MetaMode = CheckAll | CheckFirst | NoCheck
record MetaContext where
constructor MC
metas : SortedMap QName MetaEntry
autos : List QName
next : Int
mcmode : MetaMode
@@ -370,7 +371,10 @@ record ModContext where
-- A placeholder while walking through dependencies of a module
emptyModCtx : String → ModContext
emptyModCtx csum = MkModCtx csum EmptyMap (MC EmptyMap 0 NoCheck) EmptyMap
emptyModCtx csum = MkModCtx csum EmptyMap (MC EmptyMap Nil 0 NoCheck) EmptyMap
HintTable : U
HintTable = SortedMap QName (List (QName × Tm))
record TopContext where
constructor MkTop
@@ -378,6 +382,8 @@ record TopContext where
-- I'm putting a dummy entry in
modules : SortedMap (List String) ModContext
imported : List (List String)
-- TCon name → function name × type
hints : HintTable
-- current module
ns : List String