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

qn for metas

Browse Source
This commit is contained in:
Steve Dunham
2025-01-11 20:07:50 -08:00
parent 1a9a8d3312
commit 793c3a9999
9 changed files with 79 additions and 94 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
port/Lib/Common.newt
View File

@@ -96,11 +96,22 @@ emptyFC = MkFC "" (0,0)
-- Error of a parse
data QName : U where
QN : List String -> String -> QName
instance Eq QName where
QN ns n == QN ns' n' = n == n' && ns == ns'
instance Show QName where
show (QN Nil n) = n
show (QN ns n) = joinBy "." ns ++ "." ++ n
instance Ord QName where
compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
data Error
= E FC String
| Postpone FC Int String
| Postpone FC QName String
instance Show FC where
show fc = "\{fc.file}:\{show fc.start}"

45
port/Lib/Elab.newt
View File

@@ -92,8 +92,8 @@ forceMeta : Val -> M Val
forceMeta (VMeta fc ix sp) = do
meta <- lookupMeta ix
case meta of
(Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp)
(Solved _ k t) => vappSpine t sp >>= forceMeta
_ => pure (VMeta fc ix sp)
forceMeta x = pure x
@@ -199,7 +199,7 @@ makeSpine k (Defined :: xs) = makeSpine (k - 1) xs
makeSpine k (Bound :: xs) = makeSpine (k - 1) xs :< VVar emptyFC (k - 1) Lin
solve : Env -> (k : Int) -> SnocList Val -> Val -> M Unit
solve : Env -> QName -> SnocList Val -> Val -> M Unit
@@ -259,8 +259,8 @@ solveAutos : Int -> M Unit
solveAutos mstart = do
top <- get
mc <- readIORef top.metaCtx
let mlen = length' mc.metas - mstart
res <- run $ filter isAuto (ite (mstart == 0) mc.metas $ take (cast mlen) mc.metas)
res <- run $ filter isAuto (listValues mc.metas)
if res then solveAutos mstart else pure MkUnit
where
isAuto : MetaEntry -> Bool
@@ -275,20 +275,16 @@ solveAutos mstart = do
-- We need to switch to SortedMap here
updateMeta : Int -> (MetaEntry -> M MetaEntry) -> M Unit
updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit
updateMeta ix f = do
top <- get
mc <- readIORef top.metaCtx
metas <- go mc.metas
writeIORef top.metaCtx $ MC metas mc.next mc.mcmode
where
go : List MetaEntry -> M (List MetaEntry)
go Nil = error' "Meta \{show ix} not found"
go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs
go (x@((Solved _ k y)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs
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
checkAutos : Int -> List MetaEntry -> M Unit
checkAutos : QName -> List MetaEntry -> M Unit
checkAutos ix Nil = pure MkUnit
checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
ty' <- quote ctx.lvl ty
@@ -302,8 +298,7 @@ checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
checkAutos ix (_ :: rest) = checkAutos ix rest
addConstraint : Env -> Int -> SnocList Val -> Val -> M Unit
addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit
addConstraint env ix sp tm = do
top <- get
mc <- readIORef top.metaCtx
@@ -313,8 +308,9 @@ addConstraint env ix sp tm = do
debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
(Solved _ k tm) => error' "Meta \{show k} already solved (addConstraint :: Nil)"
(OutOfScope) => error' "Meta \{show ix} out of scope"
mc <- readIORef top.metaCtx
checkAutos ix mc.metas
checkAutos ix (listValues mc.metas)
-- this loops too
-- solveAutos 0 mc.metas
pure MkUnit
@@ -341,9 +337,9 @@ invert lvl sp = go sp Nil
-- I think that essentially means our domain ix are one bigger, since we're looking at lvl
-- in the codomain, so maybe we can just keep that value
rename : Int -> List Int -> Int -> Val -> M Tm
rename : QName -> List Int -> Int -> Val -> M Tm
renameSpine : Int -> List Int -> Int -> Tm -> SnocList Val -> M Tm
renameSpine : QName -> List Int -> Int -> Tm -> SnocList Val -> M Tm
renameSpine meta ren lvl tm Lin = pure tm
renameSpine meta ren lvl tm (xs :< x) = do
xtm <- rename meta ren lvl x
@@ -447,6 +443,7 @@ solve env m sp t = do
updateMeta m $ \case
(Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
(Solved _ k x) => error' "Meta \{show ix} already solved! (solve2 :: Nil)"
OutOfScope => error' "Meta \{show ix} out of scope"
maybeCheck $ for_ cons $ \case
MkMc fc env sp rhs => do
val <- vappSpine soln sp
@@ -646,11 +643,14 @@ freshMeta ctx fc ty kind = do
top <- get
mc <- readIORef top.metaCtx
debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
let newmeta = Unsolved fc mc.next ctx ty kind Nil
writeIORef top.metaCtx $ MC (newmeta :: mc.metas) (1 + mc.next) mc.mcmode
-- need the ns here
-- we were fudging this for v1
let qn = QN ("$meta" :: Nil) (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
-- infinite loop - keeps trying Ord a => Ord (a \x a)
-- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta
pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
pure $ applyBDs 0 (Meta fc qn) ctx.bds
where
-- hope I got the right order here :)
applyBDs : Int -> Tm -> List BD -> Tm
@@ -1269,6 +1269,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
-- TODO - only hit the relevant ones
ignore $ solveAutos 0
forceType ctx.env scty'
OutOfScope => pure scty'
_ => pure scty'

9
port/Lib/Eval.newt
View File

@@ -93,8 +93,9 @@ forceType : Env -> Val -> M Val
forceType env (VMeta fc ix sp) = do
meta <- lookupMeta ix
case meta of
(Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
(Solved _ k t) => vappSpine t sp >>= forceType env
_ => pure (VMeta fc ix sp)
forceType env x = do
Just x' <- tryEval env x
| _ => pure x
@@ -158,8 +159,8 @@ eval env mode (Erased fc) = pure (VErased fc)
eval env mode (Meta fc i) = do
meta <- lookupMeta i
case meta of
(Unsolved _ k xs _ _ _) => pure $ VMeta fc i Lin
(Solved _ k t) => pure $ t
_ => pure $ VMeta fc i Lin
eval env mode (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t)
eval env mode (Pi fc x icit rig a b) = do
a' <- eval env mode a
@@ -207,8 +208,8 @@ quote l (VVar fc k sp) = if k < l
quote l (VMeta fc i sp) = do
meta <- lookupMeta i
case meta of
(Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp
(Solved _ k t) => vappSpine t sp >>= quote l
_ => quoteSp l (Meta fc i) sp
quote l (VLam fc x icit rig t) = do
val <- t $$ VVar emptyFC l Lin
tm <- quote (1 + l) val
@@ -308,7 +309,7 @@ zonkApp top l env t@(Meta fc k) sp = do
foo <- vappSpine v (Lin <>< sp')
debug $ \ _ => "-> result is \{show foo}"
tweakFC fc <$> quote l foo
(Unsolved x j xs _ _ _) => pure $ appSpine t sp
_ => pure $ appSpine t sp
zonkApp top l env t sp = do
t' <- zonk top l env t
pure $ appSpine t' sp

32
port/Lib/ProcessDecl.newt
View File

@@ -33,26 +33,18 @@ dumpEnv ctx =
go names (1 + k) xs (" \{n} = \{render 90 $ pprint names v'} : \{render 90 $ pprint names ty'}":: acc)
logMetas : Int -> M Unit
logMetas mstart = do
-- FIXME, now this isn't logged for Sig / Data.
top <- get
mc <- readIORef {M} top.metaCtx
let mlen = cast {Int} {Nat} $ length' mc.metas - mstart
ignore $ for (reverse $ take mlen mc.metas) $ \case
(Solved fc k soln) => do
-- TODO put a flag on this, vscode is getting overwhelmed and
-- dropping errors
--info fc "solve \{show k} as \{render 90 $ pprint Nil !(quote 0 soln)}"
pure MkUnit
(Unsolved fc k ctx ty User cons) => do
logMetas : List MetaEntry -> M Unit
logMetas Nil = pure MkUnit
logMetas (OutOfScope :: rest) = logMetas rest
logMetas (Solved fc k soln :: rest) = logMetas rest
logMetas (Unsolved fc k ctx ty User cons :: rest) = do
ty' <- quote ctx.lvl ty
let names = map fst ctx.types
env <- dumpEnv ctx
let msg = "\{env} -----------\n \{render 90 $ pprint names ty'}"
info fc "User Hole\n\{msg}"
(Unsolved fc k ctx ty kind cons) => do
logMetas rest
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
@@ -79,7 +71,7 @@ logMetas mstart = do
_ => pure Nil
info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
-- addError $ E fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
logMetas rest
-- Used for Class and Record
@@ -120,8 +112,6 @@ processDecl ns (TypeSig fc names tm) = do
ty <- zonk top 0 Nil ty
putStrLn "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}"
ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom
-- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here
-- logMetas mstart
processDecl ns (PType fc nm ty) = do
top <- get
@@ -144,7 +134,6 @@ processDecl ns (Def fc nm clauses) = do
putStrLn "Def \{show nm}"
top <- get
mc <- readIORef top.metaCtx
let mstart = length' mc.metas
let (Just entry) = lookupRaw nm top
| Nothing => throwError $ E fc "No declaration for \{nm}"
let (MkEntry fc name ty Axiom) = entry
@@ -161,8 +150,7 @@ processDecl ns (Def fc nm clauses) = do
-- putStrLn "Ok \{render 90 $ pprint Nil tm}"
mc <- readIORef top.metaCtx
let mlen = length' mc.metas - mstart
solveAutos mstart
solveAutos 0
-- 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.
-- Day1.newt is a test case
@@ -177,7 +165,6 @@ processDecl ns (Def fc nm clauses) = do
when top.verbose $ \ _ => putStrLn "ERASED\n\{render 80 $ pprint Nil tm'}"
debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm'} : \{render 90 $ pprint Nil ty}"
updateDef (QN ns nm) fc ty (Fn tm')
-- logMetas mstart
processDecl ns (DCheck fc tm ty) = do
putStrLn "----- DCheck"
@@ -414,7 +401,6 @@ processDecl ns (Data fc nm ty cons) = do
decl => throwError $ E (getFC decl) "expected constructor declaration"
putStrLn "setDef \{nm} TCon \{show $ join cnames}"
updateDef (QN ns nm) fc tyty (TCon (join cnames))
-- logMetas mstart
where
binderName : Binder → Name
binderName (MkBinder _ nm _ _ _) = nm

2
port/Lib/TopContext.newt
View File

@@ -30,7 +30,7 @@ instance Show TopContext where
-- TODO need to get class dependencies working
emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
emptyTop = do
mcctx <- newIORef (MC Nil 0 CheckAll)
mcctx <- newIORef (MC EmptyMap 0 CheckAll)
errs <- newIORef $ the (List Error) Nil
pure $ MkTop EmptyMap mcctx False errs Nil EmptyMap

40
port/Lib/Types.newt
View File

@@ -9,19 +9,6 @@ import Data.SnocList
import Data.SortedMap
import Data.String
data QName : U where
QN : List String -> String -> QName
instance Eq QName where
QN ns n == QN ns' n' = n == n' && ns == ns'
instance Show QName where
show (QN Nil n) = n
show (QN ns n) = joinBy "." ns ++ "." ++ n
instance Ord QName where
compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
Name : U
Name = String
@@ -88,9 +75,7 @@ data Tm : U where
Bnd : FC -> Int -> Tm
-- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
Ref : FC -> QName -> Def -> Tm
Meta : FC -> Int -> Tm
-- kovacs optimization, I think we can App out meta instead
-- InsMeta : Int -> List BD -> Tm
Meta : FC -> QName -> Tm
Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm
App : FC -> Tm -> Tm -> Tm
UU : FC -> Tm
@@ -236,7 +221,7 @@ data Val : U where
-- neutral case
VCase : FC -> (sc : Val) -> List CaseAlt -> Val
-- we'll need to look this up in ctx with IO
VMeta : FC -> (ix : Int) -> (sp : SnocList Val) -> Val
VMeta : FC -> QName -> (sp : SnocList Val) -> Val
VLam : FC -> Name -> Icit -> Quant -> Closure -> Val
VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val
VLet : FC -> Name -> Val -> Val -> Val
@@ -305,7 +290,10 @@ instance Show MetaKind where
data MConstraint = MkMc FC Env (SnocList Val) Val
data MetaEntry = Unsolved FC Int Context Val MetaKind (List MConstraint) | Solved FC Int Val
data MetaEntry
= Unsolved FC QName Context Val MetaKind (List MConstraint)
| Solved FC QName Val
| OutOfScope
-- The purpose of this is to only check one level of constraints when trying an Auto solution
-- The idea being we narrow it down to the likely solution, and let any consequent type error
@@ -315,7 +303,7 @@ data MetaMode = CheckAll | CheckFirst | NoCheck
record MetaContext where
constructor MC
metas : List MetaEntry
metas : SortedMap QName MetaEntry
next : Int
mcmode : MetaMode
@@ -391,6 +379,7 @@ define (MkCtx lvl env types bds ctxFC) name val ty =
instance Show MetaEntry where
show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}"
show (Solved _ k x) = "Solved \{show k} \{show x}"
show OutOfScope = "OutOfScope"
withPos : Context -> FC -> Context
withPos (MkCtx lvl env types bds ctxFC) fc = (MkCtx lvl env types bds fc)
@@ -492,16 +481,13 @@ error fc msg = throwError $ E fc msg
error' : ∀ a. String -> M a
error' msg = throwError $ E emptyFC msg
lookupMeta : Int -> M MetaEntry
lookupMeta : QName -> M MetaEntry
lookupMeta ix = do
top <- get
mc <- readIORef top.metaCtx
go mc.metas
where
go : List MetaEntry -> M MetaEntry
go Nil = error' "Meta \{show ix} not found"
go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs
go (meta@(Solved _ k x) :: xs) = if k == ix then pure meta else go xs
mc <- readIORef {M} top.metaCtx
case lookupMap' ix mc.metas of
Just meta => pure meta
Nothing => pure OutOfScope
mkCtx : FC -> Context
mkCtx fc = MkCtx 0 Nil Nil Nil fc