From 27432840a83164a13c8eae9b02c1fb538dd22da5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 31 Aug 2024 20:45:46 -0700 Subject: [PATCH] investigating issue --- newt/Zoo1.newt | 55 +++++++++++++++++++++++++++++++++ newt/testcase2.newt | 4 +-- newt/{zoo2.newt => zoo2eg.newt} | 0 src/Lib/CaseTree.idr | 16 +++------- src/Lib/Check.idr | 14 ++++++--- src/Lib/Parser.idr | 30 +++++++++--------- src/Lib/ProcessDecl.idr | 15 +++++---- src/Lib/Syntax.idr | 1 - src/Lib/Types.idr | 4 +-- 9 files changed, 97 insertions(+), 42 deletions(-) create mode 100644 newt/Zoo1.newt rename newt/{zoo2.newt => zoo2eg.newt} (100%) diff --git a/newt/Zoo1.newt b/newt/Zoo1.newt new file mode 100644 index 0000000..3ad44e6 --- /dev/null +++ b/newt/Zoo1.newt @@ -0,0 +1,55 @@ +module Zoo1 + +-- I'm starting to translate ezoo 01-eval-closures-debruijn as a test cases. + +ptype Int +ptype String + +------- Prelude stuff + +data Nat : U where + Z : Nat + S : Nat -> Nat + +data Unit : U where + MkUnit : Unit + +data List : U -> U where + Nil : {a : U} -> List a + Cons : {a : U} -> a -> List a -> List a + +data Maybe : U -> U where + Just : {a : U} -> a -> Maybe a + Nothing : {a : U} -> Maybe a + +Val : U + +data Tm : U where + Var : Nat -> Tm + Lam : Tm -> Tm -- lam (x.t) + App : Tm -> Tm -> Tm + Let : Tm -> Tm -> Tm -- let t (x.u) + +data Env : U where + ENil : Env + Define : Env -> Val -> Env + +data Closure : U where + MkClosure : Env -> Tm -> Closure + +data Val : U where + VVar : Nat -> Val + VApp : Val -> Val -> Val + VLam : Closure -> Val + +length : Env -> Nat +length ENil = Z +length (Define env _) = S (length env) + +lookup : Env -> Nat -> Maybe Val +lookup (Define env v) Z = Just v +lookup (Define env _) (S k) = Just (lookup env k) +-- bug in unify? are the meta args backwards? It seems to quote back right.. +-- we're getting `Maybe Val` as meta3, and comparing: +-- Maybe ?m3 =?= Maybe Val +lookup (ENil) x = Nothing diff --git a/newt/testcase2.newt b/newt/testcase2.newt index a932751..8bca1b6 100644 --- a/newt/testcase2.newt +++ b/newt/testcase2.newt @@ -63,6 +63,6 @@ nand x y = not (case x of -- for stuff like this, we should add Agda () and check for no constructors data Void : U where - - +SnocList : U -> U +SnocList a = List a diff --git a/newt/zoo2.newt b/newt/zoo2eg.newt similarity index 100% rename from newt/zoo2.newt rename to newt/zoo2eg.newt diff --git a/src/Lib/CaseTree.idr b/src/Lib/CaseTree.idr index 63694e9..bc5ee01 100644 --- a/src/Lib/CaseTree.idr +++ b/src/Lib/CaseTree.idr @@ -128,14 +128,6 @@ getConstructors ctx tm = error (getValFC tm) "Not a type constructor \{show tm}" -- Extend environment with fresh variables from a pi-type -- return context, remaining type, and list of names extendPi : Context -> Val -> SnocList Bind -> M (Context, Val, List Bind) --- NEXT This doesn't work, unsound. --- We need all of these vars with icity _and_ to insert implicits in the pattern --- extendPi ctx (VPi x str Implicit a b) nms = do --- let nm = fresh "pat" --- let ctx' = extend ctx nm a --- let v = VVar emptyFC (length ctx.env) [<] --- tyb <- b $$ v --- extendPi ctx' tyb nms extendPi ctx (VPi x str icit a b) nms = do let nm = fresh "pat" let ctx' = extend ctx nm a @@ -157,9 +149,11 @@ buildCase ctx prob scnm (dcName, _, ty) = do vty <- eval [] CBN ty (ctx', ty', vars) <- extendPi ctx (vty) [<] - debug "clauses were \{show prob.clauses} (dcon \{show dcName}) (vars \{show vars})" + debug "(dcon \{show dcName}) (vars \{show vars}) clauses were" + for_ prob.clauses $ (\x => debug " \{show x}") let clauses = mapMaybe (rewriteClause vars) prob.clauses - debug " and now \{show clauses}" + debug "and now:" + for_ clauses $ (\x => debug " \{show x}") -- So ideally we'd know which position we're splitting and the surrounding context -- That might be a lot to carry forward (maybe a continuation?) but we could carry -- backwards as a List Missing that we augment as we go up. @@ -205,7 +199,7 @@ buildCase ctx prob scnm (dcName, _, ty) = do PatVar _ s => Just $ c :: (xs ++ acc) PatWild _ => Just $ c :: (xs ++ acc) PatCon _ str ys => if str == dcName - then Just $ (makeConst vars ys) ++ acc + then Just $ (makeConst vars ys) ++ xs ++ acc else Nothing else rewriteCons vars xs (c :: acc) diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index c59f58f..00e84ef 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -112,6 +112,9 @@ parameters (ctx: Context) debug " =?= \{show u}" t' <- forceMeta t u' <- forceMeta u + debug "forced \{show t'}" + debug " =?= \{show u'}" + debug "env \{show ctx.env}" case (t',u') of (VLam _ _ t, VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) (t, VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<]) @@ -121,9 +124,11 @@ parameters (ctx: Context) if k == k' then unifySpine l (k == k') sp sp' else error emptyFC "vvar mismatch \{show k} \{show k'}" (VRef fc k def sp, VRef fc' k' def' sp' ) => - if k == k' then unifySpine l (k == k') sp sp' + if k == k' then do + debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}" + unifySpine l (k == k') sp sp' -- REVIEW - consider forcing? - else error emptyFC "vref mismatch \{show k} \{show k'}" + else error emptyFC "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" (VMeta fc k sp, VMeta fc' k' sp' ) => if k == k' then unifySpine l (k == k') sp sp' else solve l k sp (VMeta fc' k' sp') @@ -136,13 +141,14 @@ parameters (ctx: Context) debug "expand \{show t} =?= %ref \{k'}" case lookup k' !(get) of Just (MkEntry name ty (Fn tm)) => unify l t !(vappSpine !(eval [] CBN tm) sp') - _ => error emptyFC "unify failed \{show t'} =?= \{show u'} [no Fn]\n env is \{show ctx.env} \{show $ map fst ctx.types}" + _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} [no Fn]\n env is \{show ctx.env} \{show $ map fst ctx.types}" -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. - _ => error emptyFC "unify failed \{show t'} =?= \{show u'} \n env is \{show ctx.env} \{show $ map fst ctx.types}" + _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} \n env is \{show ctx.env} \{show $ map fst ctx.types}" unifyCatch : FC -> Context -> Val -> Val -> M () unifyCatch fc ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do let names = toList $ map fst ctx.types + debug "fail \{show ty'} \{show ty}" a <- quote ctx.lvl ty' b <- quote ctx.lvl ty let msg = "\n failed to unify \{pprint names a}\n with \{pprint names b}\n " <+> str diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 460070e..bf3b79d 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -140,9 +140,9 @@ letExpr = do pure (name,fc,t) pLetArg : Parser (Icit, String, Maybe Raw) -pLetArg = (Implicit,,) <$> braces ident <*> optional (sym ":" >> typeExpr) - <|> (Explicit,,) <$> parens ident <*> optional (sym ":" >> typeExpr) - <|> (Explicit,,Nothing) <$> ident +pLetArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr) + <|> (Explicit,,) <$> parens (ident <|> uident) <*> optional (sym ":" >> typeExpr) + <|> (Explicit,,Nothing) <$> (ident <|> uident) <|> (Explicit,"_",Nothing) <$ keyword "_" -- lam: λ {A} {b : A} (c : Blah) d e f. something @@ -203,7 +203,7 @@ term = caseExpr ebind : Parser (List (String, Icit, Raw)) ebind = do sym "(" - names <- some ident + names <- some (ident <|> uident) sym ":" ty <- typeExpr sym ")" @@ -213,7 +213,7 @@ ibind : Parser (List (String, Icit, Raw)) ibind = do sym "{" mustWork $ do - names <- some ident + names <- some (ident <|> uident) ty <- optional (sym ":" >> typeExpr) pos <- getPos sym "}" @@ -262,7 +262,7 @@ export parseDef : Parser Decl parseDef = do fc <- getPos - nm <- ident + nm <- ident <|> uident pats <- many pPattern keyword "=" body <- mustWork typeExpr @@ -289,14 +289,16 @@ parseData : Parser Decl parseData = do fc <- getPos keyword "data" - name <- uident - keyword ":" - ty <- typeExpr - keyword "where" - commit - decls <- startBlock $ manySame $ parseSig - -- TODO - turn decls into something more useful - pure $ Data fc name ty decls + -- FIXME - switch from mustWork / commit to checking if we've consumed tokens + mustWork $ do + name <- uident + keyword ":" + ty <- typeExpr + keyword "where" + commit + decls <- startBlock $ manySame $ parseSig + -- TODO - turn decls into something more useful + pure $ Data fc name ty decls -- Not sure what I want here. -- I can't get a Tm without a type, and then we're covered by the other stuff diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index bbab321..c9b0c0d 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -37,7 +37,7 @@ processDecl (TypeSig fc nm tm) = do | _ => error fc "\{show nm} is already defined" putStrLn "-----" putStrLn "TypeSig \{nm} \{show tm}" - ty <- check (mkCtx top.metas) tm (VU fc) + ty <- check (mkCtx top.metas fc) tm (VU fc) ty' <- nf [] ty putStrLn "got \{pprint [] ty'}" modify $ setDef nm ty' Axiom @@ -47,7 +47,7 @@ processDecl (PType fc nm) = do modify $ setDef nm (U fc) PrimTCon processDecl (PFunc fc nm ty src) = do top <- get - ty <- check (mkCtx top.metas) ty (VU fc) + ty <- check (mkCtx top.metas fc) ty (VU fc) ty' <- nf [] ty putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}" modify $ setDef nm ty' (PrimFn src) @@ -69,8 +69,7 @@ processDecl (Def fc nm clauses) = do vty <- eval empty CBN ty putStrLn "vty is \{show vty}" - tm <- buildTree ({ fc := fc} $ mkCtx ctx.metas) (MkProb clauses vty) - -- tm <- check (mkCtx ctx.metas) body vty + tm <- buildTree (mkCtx ctx.metas fc) (MkProb clauses vty) putStrLn "Ok \{pprint [] tm}" mc <- readIORef ctx.metas @@ -86,10 +85,10 @@ processDecl (Def fc nm clauses) = do processDecl (DCheck fc tm ty) = do top <- get putStrLn "check \{show tm} at \{show ty}" - ty' <- check (mkCtx top.metas) tm (VU fc) + ty' <- check (mkCtx top.metas fc) tm (VU fc) putStrLn "got type \{pprint [] ty'}" vty <- eval [] CBN ty' - res <- check (mkCtx top.metas) ty vty + res <- check (mkCtx top.metas fc) ty vty putStrLn "got \{pprint [] res}" norm <- nf [] res putStrLn "norm \{pprint [] norm}" @@ -104,7 +103,7 @@ processDecl (DImport fc str) = throwError $ E fc "import not implemented" processDecl (Data fc nm ty cons) = do -- It seems like the FC for the errors are not here? ctx <- get - tyty <- check (mkCtx ctx.metas) ty (VU fc) + tyty <- check (mkCtx ctx.metas fc) ty (VU fc) -- FIXME we need this in scope, but need to update modify $ setDef nm tyty Axiom ctx <- get @@ -112,7 +111,7 @@ processDecl (Data fc nm ty cons) = do -- expecting tm to be a Pi type (TypeSig fc nm' tm) => do ctx <- get - dty <- check (mkCtx ctx.metas) tm (VU fc) + dty <- check (mkCtx ctx.metas fc) tm (VU fc) debug "dty \{nm'} is \{pprint [] dty}" -- We only check that codomain uses the right type constructor diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 35c7686..8514ff8 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -48,7 +48,6 @@ record Clause where -- it has names from Pats, which will need types in the env expr : Raw - -- could be a pair, but I suspect stuff will be added? public export data RCaseAlt = MkAlt Raw Raw diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index b1c788e..810bde0 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -378,8 +378,8 @@ M = (StateT TopContext (EitherT Impl.Error IO)) -- we need more of topcontext later - Maybe switch it up so we're not passing -- around top export -mkCtx : IORef MetaContext -> Context -mkCtx metas = MkCtx 0 [] [] [] metas emptyFC +mkCtx : IORef MetaContext -> FC -> Context +mkCtx metas fc = MkCtx 0 [] [] [] metas fc ||| Force argument and print if verbose is true export