misc cleanup

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

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

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.
+        debug "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}"
-        -- 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 "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
+  -- rendered in ProcessDecl
-  (RHole fc, ty) => do
+  (RHole fc, ty) => freshMeta ctx fc ty User
-    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
 
   (t@(RLam fc nm icit tm), ty@(VPi fc' nm' icit' a b)) => do
           debug "icits \{nm} \{show icit} \{nm'} \{show icit'}"

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
+    (Unsolved fc k ctx ty User cons) => do
-      -- TODO print here instead of during Elab
+      ty' <- quote ctx.lvl ty
-      pure ()
+      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

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 (VVar _ k sp) = "(%var \{show k} \{unwords $ map show (sp <>> [])})"
-  show (VRef _ nm _ sp) = "(%ref \{nm} \{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})"

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