From 56e005d2dcb0944aae8390a78ea421abd6aa0c0b Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 30 Oct 2024 21:22:45 -0700 Subject: [PATCH] misc cleanup --- TODO.md | 3 ++- newt/TypeClass.newt | 2 +- src/Lib/Elab.idr | 27 +++------------------------ src/Lib/ProcessDecl.idr | 12 +++++++++--- src/Lib/Types.idr | 4 ++-- tests/black/TypeClass.newt | 1 + 6 files changed, 18 insertions(+), 31 deletions(-) diff --git a/TODO.md b/TODO.md index 20119f5..8b4158b 100644 --- a/TODO.md +++ b/TODO.md @@ -3,7 +3,8 @@ - [ ] Allow unicode operators/names - refactored parser to prep for this -- [ ] handle if_then_else_ +- [ ] get rid of stray INFO from auto resolution +- [ ] handle if_then_else_j - [x] Remember operators from imports - [ ] Default cases for non-primitives (currently gets expanded to all constructors) - [x] Case for primitives diff --git a/newt/TypeClass.newt b/newt/TypeClass.newt index e47ef14..fb4e179 100644 --- a/newt/TypeClass.newt +++ b/newt/TypeClass.newt @@ -37,6 +37,7 @@ pure {_} {_} {{MkMonad _ pure'}} a = pure' a infixl 1 _>>=_ _>>_ _>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b +ma >> mb = mb ptype Int @@ -50,5 +51,4 @@ bar : Int -> Maybe Int bar x = do let y = x z <- Just x - -- This is not sorting out the Maybe... pure z diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 61298eb..b7192c7 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -179,14 +179,8 @@ parameters (ctx: Context) debug "\{show m} size is \{show size} sps \{show $ length sp}" let True = length sp == size | _ => do - -- need INFO that works like debug. - -- FIXME we probably need to hold onto the constraint and recheck when we solve the meta? - info (getFC t) "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" + debug "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" debug "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}" - -- error (getFC t) "meta \{show m} applied to \{show $ length sp} args instead of \{show size}" - --- add constraint to meta m --- we can keep a list and run them when it is solved. addConstraint ctx m sp t debug "meta \{show meta}" @@ -201,12 +195,10 @@ parameters (ctx: Context) putStrLn "INFO at \{show pos}: solve \{show k} as \{pprint [] !(quote 0 soln)}" pure $ Solved k soln (Solved k x) => error' "Meta \{show ix} already solved!" - -- We're not breaking anything, but not quite getting an answer? for_ cons $ \case MkMc fc ctx sp rhs => do val <- vappSpine soln sp debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}" - -- is this the right depth? unify ctx.lvl val rhs pure () @@ -852,21 +844,8 @@ check ctx tm ty = case (tm, !(forceType ty)) of let ctx' = extend ctx scnm scty pure $ Let fc scnm sc !(buildTree ctx' $ MkProb clauses ty) - -- Document a hole, pretend it's implemented - (RHole fc, ty) => do - ty' <- quote ctx.lvl ty - let names = (toList $ map fst ctx.types) - -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. - env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}" - let msg = unlines (toList $ reverse env) ++ " -----------\n" ++ " goal \{pprint names ty'}" - info fc "\n\{msg}" - -- let context = unlines foo - -- need to print 'warning' with position - -- fixme - just put a name on it like idris and stuff it into top. - -- error [DS "hole:\n\{msg}"] - -- TODO mark this meta as a user hole - -- freshMeta ctx fc - pure $ Ref fc "?" Axiom + -- rendered in ProcessDecl + (RHole fc, ty) => freshMeta ctx fc ty User (t@(RLam fc nm icit tm), ty@(VPi fc' nm' icit' a b)) => do debug "icits \{nm} \{show icit} \{nm'} \{show icit'}" diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 471d3a2..a9e531a 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -152,15 +152,21 @@ processDecl (Def fc nm clauses) = do let mlen = length mc.metas `minus` mstart solveAutos mlen (take mlen mc.metas) + -- Expand metas + -- tm' <- nf [] tm -- TODO - nf that expands all metas, Day1.newt is a test case tm' <- zonk top 0 [] tm putStrLn "NF \{pprint[] tm'}" mc <- readIORef top.metas for_ (take mlen mc.metas) $ \case (Solved k x) => pure () - (Unsolved (l,c) k ctx ty User cons) => do - -- TODO print here instead of during Elab - pure () + (Unsolved fc k ctx ty User cons) => do + ty' <- quote ctx.lvl ty + let names = (toList $ map fst ctx.types) + -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. + env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}" + let msg = "\{unlines (toList $ reverse env)} -----------\n goal \{pprint names ty'}" + info fc "User Hole\n\{msg}" (Unsolved (l,c) k ctx ty kind cons) => do tm <- quote ctx.lvl !(forceMeta ty) -- Now that we're collecting errors, maybe we simply check at the end diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index abf3910..9481651 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -251,8 +251,8 @@ Show Closure covering export Show Val where - show (VVar _ k sp) = "(%var \{show k} \{show sp})" - show (VRef _ nm _ sp) = "(%ref \{nm} \{show sp})" + show (VVar _ k sp) = "(%var \{show k} \{unwords $ map show (sp <>> [])})" + show (VRef _ nm _ sp) = "(%ref \{nm} \{unwords $ map show (sp <>> [])})" show (VMeta _ ix sp) = "(%meta \{show ix} \{show $ length sp})" show (VLam _ str x) = "(%lam \{str} \{show x})" show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show x}}. \{show y})" diff --git a/tests/black/TypeClass.newt b/tests/black/TypeClass.newt index e28b09c..d99b6b0 100644 --- a/tests/black/TypeClass.newt +++ b/tests/black/TypeClass.newt @@ -37,6 +37,7 @@ pure {_} {_} {{MkMonad _ pure'}} a = pure' a infixl 1 _>>=_ _>>_ _>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b +ma >> mb = mb ptype Int