Zonk metas in functions, optional type signature on ptype

src/Lib/Check.idr

@@ -283,7 +283,7 @@ findSplit (_ :: xs) = findSplit xs
 
 -- we could pass into build case and use it for   (x /? y)
 
--- TODO, we may need to filter these for the situation.
+-- TODO, we may need to filter these for the type
 getConstructors : Context -> Val -> M (List (String, Nat, Tm))
 getConstructors ctx (VRef fc nm _ _) = do
   names <- lookupTCon nm
@@ -312,10 +312,8 @@ extendPi ctx (VPi x str icit a b) nms = do
     extendPi ctx' tyb (nms :< MkBind nm icit a)
 extendPi ctx ty nms = pure (ctx, ty, nms <>> [])
 
--- filter clause
-
--- FIXME - I don't think we're properly noticing
-
+-- turn vars into lets for forced values.
+-- Maybe we need to do more? revist the paper.
 updateContext : Context -> List (Nat, Val) -> M Context
 updateContext ctx [] = pure ctx
 updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in
@@ -350,7 +348,6 @@ buildCase ctx prob scnm scty (dcName, _, ty) = do
 
   -- I think I'm going down a different road than Idris..
 
-
   -- do this or see how other people manage?
   -- this puts the failure on the LHS
   -- unifying these should say say VVar 1 is Nat.

src/Lib/Parser.idr

@@ -272,7 +272,14 @@ parseDef = do
 
 export
 parsePType : Parser Decl
-parsePType = PType <$> getPos <* keyword "ptype" <*> uident
+parsePType = do
+  fc <- getPos
+  keyword "ptype"
+  id <- uident
+  ty <- optional $ do
+    keyword ":"
+    mustWork typeExpr
+  pure $ PType fc id ty
 
 parsePFunc : Parser Decl
 parsePFunc = do

src/Lib/Prettier.idr

@@ -16,6 +16,10 @@ data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
 ||| The capitalization is the opposite of the paper.
 data DOC = EMPTY | TEXT String DOC | LINE Nat DOC
 
+export
+empty : Doc
+empty = Empty
+
 flatten : Doc -> Doc
 flatten Empty = Empty
 flatten (Seq x y) = Seq (flatten x) (flatten y)

src/Lib/ProcessDecl.idr

@@ -36,13 +36,16 @@ processDecl (TypeSig fc nm tm) = do
   putStrLn "-----"
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas fc) tm (VU fc)
+  putStrLn "got \{pprint [] ty}"
   ty' <- nf [] ty
-  putStrLn "got \{pprint [] ty'}"
+  putStrLn "nf \{pprint [] ty'}"
   modify $ setDef nm ty' Axiom
 
-processDecl (PType fc nm) = do
+processDecl (PType fc nm ty) = do
   ctx <- get
-  modify $ setDef nm (U fc) PrimTCon
+  ty' <- check (mkCtx ctx.metas fc) (maybe (RU fc) id ty) (VU fc)
+  modify $ setDef nm ty' PrimTCon
+
 processDecl (PFunc fc nm ty src) = do
   top <- get
   ty <- check (mkCtx top.metas fc) ty (VU fc)
@@ -69,7 +72,8 @@ processDecl (Def fc nm clauses) = do
 
   tm <- buildTree (mkCtx ctx.metas fc) (MkProb clauses vty)
   putStrLn "Ok \{pprint [] tm}"
-
+  tm' <- zonk ctx 0 [] tm
+  putStrLn "NF \{pprint[] tm'}"
   mc <- readIORef ctx.metas
   for_ mc.metas $ \case
     (Solved k x) => pure ()
@@ -77,8 +81,8 @@ processDecl (Def fc nm clauses) = do
       -- should just print, but it's too subtle in the sea of messages
       -- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}"
       throwError $ E (l,c) "Unsolved meta \{show k}"
-  debug "Add def \{nm} \{pprint [] tm} : \{pprint [] ty}"
-  modify $ setDef nm ty (Fn tm)
+  debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
+  modify $ setDef nm ty (Fn tm')
 
 processDecl (DCheck fc tm ty) = do
   top <- get

src/Lib/Syntax.idr

@@ -95,7 +95,7 @@ data Decl
   | DImport FC Name
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
-  | PType FC Name
+  | PType FC Name (Maybe Raw)
   | PFunc FC Name Raw String
 
 
@@ -134,7 +134,7 @@ Show Decl where
   show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys]
   show (DImport _ str) = foo ["DImport", show str]
   show (DCheck _ x y) = foo ["DCheck", show x, show y]
-  show (PType _ name) = foo ["PType", name]
+  show (PType _ name ty) = foo ["PType", name, show ty]
   show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src]
 
 export covering
@@ -230,5 +230,5 @@ Pretty Module where
         -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
         doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
         doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
-        doDecl (PType _ nm) = text "ptype" <+> text nm
+        doDecl (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
         doDecl (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))

src/Lib/TT.idr

@@ -241,3 +241,57 @@ solveMeta ctx ix tm = do
       then error' "Meta \{show ix} already solved!"
       else go xs (lhs :< meta)
 
+
+-- REVIEW - might be easier if we inserted the meta without a bunch of explicit App
+
+-- we need to walk the whole thing
+-- meta in Tm have a bunch of args, which should be the relevant
+-- parts of the scope. So, meta has a bunch of lambdas, we've got a bunch of
+-- args and we need to beta reduce, which seems like a lot of work for nothing
+-- Could we put the "good bits" of the Meta in there and write it to Bnd directly
+-- off of scope? I guess this might get dicey when a meta is another meta applied
+-- to something.
+
+-- ok, so we're doing something that looks lot like eval, having to collect args,
+-- pull the def, and apply spine. Eval is trying for WHNF, so it doesn't walk the
+-- whole thing. (We'd like to insert metas inside lambdas.)
+export
+zonk : TopContext -> Nat -> Env -> Tm -> M Tm
+
+zonkBind : TopContext -> Nat -> Env -> Tm -> M Tm
+zonkBind top l env tm = zonk top (S l) (VVar (getFC tm) l [<] :: env) tm
+
+-- I don't know if app needs an FC...
+
+appSpine : Tm -> List Tm -> Tm
+appSpine t [] = t
+appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs
+
+zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm
+zonkApp top l env (App fc t u) sp = zonkApp top l env t (!(zonk top l env u) :: sp)
+zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
+  (Solved j v) => do
+    sp' <- traverse (eval env CBN) sp
+    debug "zonk \{show k} -> \{show v} spine \{show sp'}"
+    foo <- vappSpine v ([<] <>< sp')
+    debug "-> result is \{show foo}"
+    quote l foo
+  (Unsolved x j xs) => pure $ appSpine t sp
+zonkApp top l env t sp = pure $ appSpine !(zonk top l env t) sp
+
+zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt
+zonkAlt top l env (CaseDefault t) = CaseDefault <$> zonkBind top l env t
+zonkAlt top l env (CaseCons name args t) = CaseCons name args <$> go l env args t
+  where
+    go : Nat -> Env -> List String -> Tm -> M Tm
+    go l env [] tm = zonk top l env t
+    go l env (x :: xs) tm = go (S l) (VVar (getFC tm) l [<] :: env) xs tm
+
+zonk top l env t = case t of
+  (Meta fc k) => zonkApp top l env t []
+  (Lam fc nm u) => Lam fc nm <$> (zonk top (S l) (VVar fc l [<] :: env) u)
+  (App fc t u) => zonkApp top l env t [!(zonk top l env u)]
+  (Pi fc nm icit a b) => Pi fc nm icit <$> zonk top l env a <*> zonkBind top l env b
+  (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u
+  (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts
+  _ => pure t

src/Main.idr

@@ -35,7 +35,7 @@ dumpContext top = do
   where
     go : List TopEntry -> M ()
     go [] = pure ()
-    go (x :: xs) = go xs >> putStrLn "    \{show x}"
+    go (x :: xs) = putStrLn "    \{show x}" >> go xs
 
 dumpSource : M ()
 dumpSource = do