From 363f85710f81c46e1449bbdb16b2bd535627d3b0 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 10 Jan 2025 21:03:20 -0800 Subject: [PATCH] add comments, fix fc on an error, add constructor for U --- TODO.md | 2 ++ port/Lib/Elab.newt | 28 ++++++++++++++++------------ port/Lib/ProcessDecl.newt | 8 ++++---- src/Lib/Elab.idr | 4 +--- src/Main.idr | 5 +++-- 5 files changed, 26 insertions(+), 21 deletions(-) diff --git a/TODO.md b/TODO.md index a5501ad..6303a86 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,8 @@ ## TODO +- [ ] review pattern matching. goal is to have a sane context on the other end. secondary goal - bring it closer to the paper. + - [x] redo code to determine base path - [ ] save/load results of processing a module - [ ] keep each module separate in context diff --git a/port/Lib/Elab.newt b/port/Lib/Elab.newt index 8ff9dd1..c4b3181 100644 --- a/port/Lib/Elab.newt +++ b/port/Lib/Elab.newt @@ -951,7 +951,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do makeConstr : List Bind -> List Pattern -> M (List (String × Pattern)) makeConstr Nil Nil = pure $ Nil -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$> - makeConstr Nil (pat :: pats) = error ctx.ctxFC "too many patterns" + makeConstr Nil (pat :: pats) = error (getFC pat) "too many patterns" makeConstr ((MkBind nm Implicit x) :: xs) Nil = do rest <- makeConstr xs Nil pure $ (nm, PatWild emptyFC Implicit) :: rest @@ -1017,19 +1017,21 @@ splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args) splitArgs tm args = (tm, args) -mkPat : TopContext -> (Raw × Icit) -> M Pattern -mkPat top (RAs fc as tm, icit) = do - pat <- mkPat top (tm, icit) +mkPat : (Raw × Icit) -> M Pattern +mkPat (RAs fc as tm, icit) = do + + pat <- mkPat (tm, icit) case pat of (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as) (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}" t => error fc "Can't put as on non-constructor \{show tm}" -mkPat top (tm, icit) = do +mkPat (tm, icit) = do + top <- get case splitArgs tm Nil of ((RVar fc nm), b) => case lookupRaw nm top of (Just (MkEntry _ name type (DCon k str))) => do -- TODO check arity, also figure out why we need reverse - bpat <- traverse (mkPat top) b + bpat <- traverse (mkPat) b pure $ PatCon fc icit name bpat Nothing -- This fires when a global is shadowed by a pattern var -- Just _ => error (getFC tm) "\{show nm} is not a data constructor" @@ -1044,10 +1046,10 @@ mkPat top (tm, icit) = do -makeClause : TopContext -> (Raw × Raw) -> M Clause -makeClause top (lhs, rhs) = do +makeClause : (Raw × Raw) -> M Clause +makeClause (lhs, rhs) = do let (nm, args) = splitArgs lhs Nil - pats <- traverse (mkPat top) args + pats <- traverse mkPat args pure $ MkClause (getFC lhs) Nil pats rhs @@ -1069,7 +1071,7 @@ checkWhere ctx decls body ty = do unless (name == name') $ \ _ => error defFC "Expected def for \{name}" -- REVIEW is this right, cribbed from my top level code top <- get - clauses' <- traverse (makeClause top) clauses + clauses' <- traverse makeClause clauses vty <- eval ctx.env CBN funTy debug $ \ _ => "\{name} vty is \{show vty}" let ctx' = extend ctx name vty @@ -1087,7 +1089,7 @@ checkWhere ctx decls body ty = do ty' <- checkWhere ctx' decls' body ty pure $ LetRec sigFC name funTy tm ty' - +-- checks the body after we're done with a case tree branch checkDone : Context -> List (String × Pattern) -> Raw -> Val -> M Tm checkDone ctx Nil body ty = do debug $ \ _ => "DONE-> check body \{show body} at \{show ty}" @@ -1264,6 +1266,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do (Unsolved _ k xs _ _ _) => do top <- get mc <- readIORef top.metaCtx + -- TODO - only hit the relevant ones ignore $ solveAutos 0 forceType ctx.env scty' @@ -1277,6 +1280,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do -- default cases cons <- getConstructors ctx (getFC pat) scty' debug $ \ _ => "CONS \{show $ map fst cons}" + -- TODO collect the wild-card only cases into one alts <- traverse (buildCase ctx prob scnm scty') cons debug $ \ _ => "GOTALTS \{show alts}" when (length' (mapMaybe id alts) == 0) $ \ _ => error (fc) "no alts for \{show scty'}" @@ -1353,7 +1357,7 @@ check ctx tm ty = do top <- get clauses <- for alts $ \case (MkAlt pat rawRHS) => do - pat' <- mkPat top (pat, Explicit) + pat' <- mkPat (pat, Explicit) pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS -- buildCase expects scrutinee to be a name in the context, so we need to let it. -- if it's a Bnd and not shadowed we could skip the let, but that's messy. diff --git a/port/Lib/ProcessDecl.newt b/port/Lib/ProcessDecl.newt index a079a66..e6515c6 100644 --- a/port/Lib/ProcessDecl.newt +++ b/port/Lib/ProcessDecl.newt @@ -139,7 +139,7 @@ processDecl ns (PFunc fc nm used ty src) = do _ => pure MkUnit setDef (QN ns nm) fc ty' (PrimFn src used) -processDecl ns (Def fc nm claused) = do +processDecl ns (Def fc nm clauses) = do putStrLn "-----" putStrLn "Def \{show nm}" top <- get @@ -155,16 +155,16 @@ processDecl ns (Def fc nm claused) = do debug $ \ _ => "\{nm} vty is \{show vty}" - -- I can take LHS apart syntactically or elaborate it with an infer - claused' <- traverse (makeClause top) claused - tm <- buildTree (mkCtx fc) (MkProb claused' vty) + clauses' <- traverse makeClause clauses + tm <- buildTree (mkCtx fc) (MkProb clauses' vty) -- putStrLn "Ok \{render 90 $ pprint Nil tm}" mc <- readIORef top.metaCtx let mlen = length' mc.metas - mstart solveAutos mstart -- 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 -- tm' <- nf Nil tm tm' <- zonk top 0 Nil tm diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index b45f824..611f3be 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -889,11 +889,9 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do makeConstr : List Bind -> List Pattern -> M (List (String, Pattern)) makeConstr [] [] = pure $ [] - -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$> - makeConstr [] (pat :: pats) = error ctx.ctxFC "too many patterns" + makeConstr [] (pat :: pats) = error (getFC pat) "too many patterns" makeConstr ((MkBind nm Implicit x) :: xs) [] = pure $ (nm, PatWild emptyFC Implicit) :: !(makeConstr xs []) makeConstr ((MkBind nm Auto x) :: xs) [] = pure $ (nm, PatWild emptyFC Auto) :: !(makeConstr xs []) - -- FIXME need a proper error, but requires wiring M three levels down makeConstr ((MkBind nm Explicit x) :: xs) [] = error ctx.ctxFC "not enough patterns" makeConstr ((MkBind nm Explicit x) :: xs) (pat :: pats) = if getIcit pat == Explicit diff --git a/src/Main.idr b/src/Main.idr index bd6842a..aa8d590 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -55,8 +55,9 @@ writeSource fn = do docs <- compile let src = unlines $ [ "\"use strict\";" - , "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" ] - ++ map (render 90) docs + , "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" + , "const U = { tag: \"U\" };" + ] ++ map (render 90) docs Right _ <- writeFile fn src | Left err => fail (show err) Right _ <- chmodRaw fn 493 | Left err => fail (show err)