From bcf34c09416c353991eaaaf869ed6bbbd0c4c87d Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 27 Jul 2025 14:50:37 -0700 Subject: [PATCH] [ auto ] try autos if a meta in their type is solved Also cut tryEval if the result is a lambda --- newt/Prelude.newt | 4 +++ src/Lib/Elab.newt | 80 ++++++++++++++++++++++++++------------------ src/Lib/Eval.newt | 1 + src/Lib/Parser.newt | 1 + src/Lib/Types.newt | 15 +++++++++ tests/RunLength.newt | 64 +++++++++++++++++++++++++++++++++++ 6 files changed, 132 insertions(+), 33 deletions(-) create mode 100644 tests/RunLength.newt diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 5c93695..fe86a2d 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -382,6 +382,10 @@ instance Show String where instance Show Int where show = showInt +instance Show Bool where + show True = "true" + show False = "false" + pfunc ord : Char → Int := `(c) => c.charCodeAt(0)` pfunc chr : Int → Char := `(c) => String.fromCharCode(c)` diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 0f5a657..9afdd06 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -117,7 +117,7 @@ setMetaMode : MetaMode → M Unit -- ideally we could do metaCtx.mcmode := CheckFirst setMetaMode mcmode = modifyTop $ \top => [ metaCtx := [mcmode := mcmode] (top.metaCtx) ] top -findMatches : Context -> Val -> List (QName × Tm) -> M (List String) +findMatches : Context -> Val -> List (QName × Tm) -> M (List QName) findMatches ctx ty Nil = pure Nil findMatches ctx ty ((name, type) :: xs) = do let (True) = isCandidate ty type @@ -137,7 +137,7 @@ findMatches ctx ty ((name, type) :: xs) = do tm <- check ctx (RVar fc nm) ty debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}" modifyTop [ metaCtx := mc ] - (_::_ nm) <$> findMatches ctx ty xs) + (_::_ name) <$> findMatches ctx ty xs) (\ err => do debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}" modifyTop [ metaCtx := mc ] @@ -189,27 +189,35 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do top <- getTop Nil <- contextMatches ctx ty | ((tm, vty) :: Nil) => do - unifyCatch (getFC ty) ctx ty vty val <- eval ctx.env CBN tm - debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}" + debug $ \ _ => "LOCAL SOLUTION \{rpprint Nil tm} evaled to \{show val}" let sp = makeSpine ctx.lvl ctx.bds solve ctx.env k sp val + debug $ \ _ => "<-- AUTO LOCAL" + debug $ \ _ => ">UNIFY \{show k}" + -- Causes infinite loop if we do this before the solve + -- may be nice to push it into solve, but vty is not there.. + unifyCatch (getFC ty) ctx ty vty + debug $ \ _ => " do - debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}" + debug $ \ _ => "LOCAL FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}" pure False 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}" + debug $ \ _ => "GLOBAL FAILED to solve \{show ty}, matches: \{show res}" pure False - tm <- check ctx (RVar fc nm) ty - val <- eval ctx.env CBN tm - debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}" + let val = VRef fc nm Lin + debug $ \ _ => "GLOBAL SOLUTION \{show val}" let sp = makeSpine ctx.lvl ctx.bds solve ctx.env k sp val + debug $ \ _ => ">CHECK \{show k}" + let (QN ns nm) = nm + ignore $ check ctx (RVar fc nm) ty + debug $ \ _ => " mc.autos modifyTop [ metaCtx := MC (updateMap ix me mc.metas) autos mc.next mc.mcmode ] -checkAutos : QName -> List MetaEntry -> M Unit +-- Try to solve autos that reference the meta ix +checkAutos : QName -> List QName -> M Unit checkAutos ix Nil = pure MkUnit -checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do - ty' <- quote ctx.lvl ty - when (usesMeta ty') $ \ _ => ignore $ trySolveAuto entry +checkAutos ix (cand :: rest) = do + entry@(Unsolved fc k ctx ty AutoSolve _) <- lookupMeta cand | _ => checkAutos ix rest + case ty of + VRef _ nm sp => if checkMeta sp + then trySolveAuto entry >> checkAutos ix rest + else pure MkUnit + _ => pure MkUnit checkAutos ix rest where - usesMeta : Tm -> Bool - usesMeta (App _ (Meta _ k) u) = if k == ix then True else usesMeta u - usesMeta (App _ _ u) = usesMeta u - usesMeta _ = False + checkMeta : SnocList Val → Bool + checkMeta Lin = False + checkMeta (sp :< VMeta _ nm _) = if nm == ix then True else checkMeta sp + checkMeta (sp :< _) = checkMeta sp + checkAutos ix (_ :: rest) = checkAutos ix rest addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit @@ -266,12 +280,8 @@ addConstraint env ix sp tm = do (Unsolved pos k a b c cons) => 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]" + (Solved fc k tm) => error fc "Meta \{show k} already solved [addConstraint]" (OutOfScope) => error' "Meta \{show ix} out of scope" - -- I broke this while dropping IORef and it seemed to have no effect - -- top <- getTop - -- let mc = top.metaCtx - -- 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,6 +363,7 @@ unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult .boundNames : Context -> List String ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst ctx.types) +-- run action if mcmode allows it, ratcheting as necessary maybeCheck : M Unit -> M Unit maybeCheck action = do top <- getTop @@ -392,13 +403,19 @@ 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]" + (Solved fc k x) => error fc "Meta \{show ix} already solved! [solve2]" OutOfScope => error' "Meta \{show ix} out of scope" - maybeCheck $ for_ cons $ \case - MkMc fc env sp rhs => do - val <- vappSpine soln sp - debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}" - unify env UNormal val rhs + maybeCheck $ do + for_ cons $ \case + MkMc fc env sp rhs => do + val <- vappSpine soln sp + debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}" + unify env UNormal val rhs + -- check any autos + top <- getTop + let mc = top.metaCtx + debug $ \ _ => "check autos depending on \{show ix} \{debugStr mc.mcmode}" + checkAutos ix mc.autos pure MkUnit ) @@ -478,7 +495,7 @@ unify env mode t u = do | Just v => unify env mode t' v if k == k' then unifySpine env mode (k == k') sp sp' - else error fc "vref mismatch \{show t'} \{show u'}" + else error fc "vref mismatch \{show t'} =?= \{show u'}" -- Lennart.newt cursed type references itself -- We _could_ look up the ref, eval against Nil and vappSpine... @@ -601,8 +618,7 @@ freshMeta ctx fc ty kind = do AutoSolve => qn :: mc.autos _ => mc.autos modifyTop $ \top => [metaCtx := MC (updateMap qn newmeta mc.metas) autos (1 + mc.next) mc.mcmode ] top - -- infinite loop - keeps trying Ord a => Ord (a \x a) - -- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta + -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet. pure $ applyBDs 0 (Meta fc qn) ctx.bds where -- hope I got the right order here :) @@ -1308,8 +1324,6 @@ undo prev ((DoArrow fc left right alts) :: xs) = do (RLam fc (BI fc nm Explicit Many) rest) Explicit - - -- REVIEW do we want to let arg? -- collect fields and default assignment -- subst in real assignment diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt index f099019..cdf4128 100644 --- a/src/Lib/Eval.newt +++ b/src/Lib/Eval.newt @@ -79,6 +79,7 @@ tryEval env (VRef fc k sp) = do val <- vappSpine vtm sp case val of VCase _ _ _ => pure Nothing + VLam _ _ _ _ _ => pure Nothing -- For now? There is a spot in Compile.newt that has -- two applications of fresh that is getting unfolded even -- though it has the same head and spine. Possibly because it's diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index b49b78d..dff3dc3 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -367,6 +367,7 @@ doArrow = do (Just _) <- optional $ keyword "<-" | _ => pure $ DoExpr fc left right <- term + -- FIXME bad error for `| pure MkUnit`, we need to commit if indentation is correct. alts <- startBlock $ manySame $ symbol "|" *> caseAlt pure $ DoArrow fc left right alts diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 74eb7d2..e405571 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -286,10 +286,19 @@ instance Show MetaKind where show User = "User" show AutoSolve = "Auto" +instance Eq MetaKind where + Normal == Normal = True + User == User = True + AutoSolve == AutoSolve = True + _ == _ = False + -- constrain meta applied to val to be a val data MConstraint = MkMc FC Env (SnocList Val) Val +instance Show MConstraint where + show (MkMc fc env (args) ty) = "MkMC \{show fc} env \{show args} \{show ty}" + data MetaEntry = Unsolved FC QName Context Val MetaKind (List MConstraint) | Solved FC QName Val @@ -308,6 +317,12 @@ record MetaContext where next : Int mcmode : MetaMode +instance Eq MetaMode where + CheckAll == CheckAll = True + CheckFirst == CheckFirst = True + NoCheck == NoCheck = True + _ == _ = False + data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon instance Eq ConInfo where diff --git a/tests/RunLength.newt b/tests/RunLength.newt new file mode 100644 index 0000000..dd89740 --- /dev/null +++ b/tests/RunLength.newt @@ -0,0 +1,64 @@ +-- This showed a couple of issues related to having ++ in types. + +module RunLength + +-- https://youtu.be/N4Z45Xg6_oc?t=1246 + +import Prelude + +-- TODO this belongs in a library + +data Void : U where + +Not : U → U +Not x = x → Void + +data Dec : U → U where + Yes : ∀ prop. (prf : prop) → Dec prop + No : ∀ prop. (contra : Not prop) → Dec prop + +class DecEq t where + decEq : (x₁ : t) → (x₂ : t) → Dec (x₁ ≡ x₂) + +-- end lib + +rep : ∀ a. Nat → a → List a +rep Z x = Nil +rep (S k) x = x :: rep k x + +data RunLength : ∀ ty. List ty → U where + Empty : ∀ ty. RunLength {ty} Nil + Run : ∀ ty more. (n : Nat) → + (x : ty) → + RunLength more → + RunLength (rep n x ++ more) + +-- Idris has `?` here, but we're allowing metas on signatures to be solved later +testComp : RunLength {Char} _ +testComp = Run (S (S (S Z))) 'x' $ Run (S (S (S (S Z)))) 'y' $ Empty + +-- 24:20 +uncompress : ∀ ty xs. RunLength {ty} xs → List ty + +data Singleton : ∀ a. a → U where + Val : ∀ a. (x : a) → Singleton x + +-- Idris generates this +-- uncompress' : ∀ ty xs. RunLength {ty} xs → Singleton xs +-- uncompress' Empty = Val Nil +-- uncompress' (Run n x y) = let (Val ys) = uncompress' y in Val (rep n x ++ _) + +solve : ∀ a. {{a}} -> a +solve {{a}} = a + +-- adding ys back in, we still get a unification failure. +-- I think because the meta for ++ is not yet solved. +uncompress' : ∀ ty xs. RunLength {ty} xs → Singleton {List ty} xs +uncompress' Empty = Val Nil +uncompress' {ty} (Run n x y) = let (Val ys) = uncompress' y in Val (rep n x ++ ys) + +rle : ∀ a. {{DecEq a}} → (xs : List a) → RunLength xs + + + +