From c6653106533d1c6e8b0b13fe2bd644623ee2561a Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 19 Nov 2024 20:50:52 -0800 Subject: [PATCH] Address issues with unify's case tree in idris Clean up some stuff in prelude Add parser for where --- Makefile | 3 +- aoc2023/Day1.newt | 2 +- aoc2023/Lib.newt | 2 +- port/Prelude.newt | 24 +++++++++-- port/Prettier.newt | 9 ++-- port/TestPrettier.newt | 1 + src/Lib/Compile.idr | 2 +- src/Lib/Elab.idr | 91 +++++++++++++++++++++-------------------- src/Lib/Parser.idr | 4 ++ src/Lib/ProcessDecl.idr | 1 - 10 files changed, 81 insertions(+), 58 deletions(-) diff --git a/Makefile b/Makefile index 681d79f..1ea5353 100644 --- a/Makefile +++ b/Makefile @@ -2,8 +2,7 @@ SRCS=$(shell find src -name "*.idr") .PHONY: -all: build/exec/newt build/exec/newt.js -# build/exec/newt.min.js +all: build/exec/newt build/exec/newt.js build/exec/newt.min.js build/exec/newt: ${SRCS} idris2 --build newt.ipkg diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt index 63d2957..3338b6c 100644 --- a/aoc2023/Day1.newt +++ b/aoc2023/Day1.newt @@ -59,7 +59,7 @@ runFile fn = let text = readFile fn in log fn >> log "part1" >> - log (part1 text (digits1 ∘ unpack)) >> + log (part1 text (digits1 ∘ unpack)) >> log "part2" >> log (part1 text (digits2 ∘ unpack)) >> log "" diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt index d59ccbf..f90c397 100644 --- a/aoc2023/Lib.newt +++ b/aoc2023/Lib.newt @@ -159,4 +159,4 @@ map f (x :: xs) = f x :: map f xs infixl 9 _∘_ _∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C -(f . g) x = f ( g x) +(f ∘ g) x = f (g x) diff --git a/port/Prelude.newt b/port/Prelude.newt index 06c3b70..5edf091 100644 --- a/port/Prelude.newt +++ b/port/Prelude.newt @@ -109,6 +109,13 @@ instance Functor Maybe where map f Nothing = Nothing map f (Just a) = Just (f a) +-- TODO this probably should depend on / entail Functor +infixl 3 _<*>_ +class Applicative (f : U → U) where + -- appIsFunctor : Functor f + return : {a} → a → f a + _<*>_ : {a b} -> f (a → b) → f a → f b + infixr 2 _<|>_ class Alternative (m : U → U) where _<|>_ : {a} → m a → m a → m a @@ -185,9 +192,17 @@ pfunc alen : {a : U} -> Array a -> Int := "(a,arr) => arr.length" pfunc aget : {a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]" pfunc aempty : {a : U} -> Unit -> Array a := "() => []" - +-- TODO represent Nat as number at runtime +pfunc natToInt : Nat -> Int := "(n) => { + let rval = 0 + while (n.tag === 'S') { + n = n.h0 + rval++ + } + return rval +}" pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')" -pfunc replicate : Nat -> Char → String := "() => abort('FIXME replicate')" +pfunc replicate : Nat -> Char → String := "(n,c) => c.repeat(natToInt(n))" -- I don't want to use an empty type because it would be a proof of void ptype World @@ -203,7 +218,10 @@ instance Monad IO where MkIORes a w => mab a w pure a = \ w => MkIORes a w -pfunc putStrLn : String -> IO Unit := "(s) => (w) => console.log(s)" +pfunc putStrLn : String -> IO Unit := "(s) => (w) => { + console.log(s) + return MkIORes(Unit,MkUnit,w) +}" class Show a where show : a → String diff --git a/port/Prettier.newt b/port/Prettier.newt index 05d4b5b..59df4e6 100644 --- a/port/Prettier.newt +++ b/port/Prettier.newt @@ -86,8 +86,8 @@ pretty {{MkPretty p}} x = p x render : Nat -> Doc -> String render w x = layout (best w Z x) Lin -SemigroupDoc : Semigroup Doc -SemigroupDoc = MkSemi (\ x y => Seq x (Seq (Text " ") y)) +instance Semigroup Doc where + x <+> y = Seq x (Seq (Text " ") y) -- Match System.File so we don't get warnings @@ -100,9 +100,8 @@ text = Text nest : Nat -> Doc -> Doc nest = Nest -infixl 7 _++_ -_++_ : Doc -> Doc -> Doc -x ++ y = Seq x y +instance Concat Doc where + x ++ y = Seq x y infixl 5 __ __ : Doc -> Doc -> Doc diff --git a/port/TestPrettier.newt b/port/TestPrettier.newt index cdabe69..60f89be 100644 --- a/port/TestPrettier.newt +++ b/port/TestPrettier.newt @@ -17,3 +17,4 @@ foo = render fifty doc main : IO Unit main = do putStrLn foo + putStrLn $ replicate five 'x' diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index c66a41d..d078d7f 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -155,7 +155,7 @@ termToJS env (CCase t alts) f = (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts)) --- REVIEW the escaping in show might not match JS +-- FIXME escaping is wrong, e.g. \215 instead of \xd7 jsString : String -> Doc jsString str = text (show str) diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index f0746fd..e94bf0e 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -232,6 +232,10 @@ unifySpine env mode True [<] [<] = pure (MkResult []) unifySpine env mode True (xs :< x) (ys :< y) = [| unify env mode x y <+> (unifySpine env mode True xs ys) |] unifySpine env mode True _ _ = error emptyFC "meta spine length mismatch" + + + + unify env mode t u = do debug "Unify lvl \{show $ length env}" debug " \{show t}" @@ -243,67 +247,55 @@ unify env mode t u = do debug "env \{show env}" -- debug "types \{show $ ctx.types}" let l = length env - case (mode,t',u') of + -- On the LHS, variable matching is yields constraints/substitutions + -- We want this to happen before VRefs are expanded, and mixing mode + -- into the case tree explodes it further. + case mode of + Pattern => unifyPattern t' u' + Normal => unify' t' u' + where + unify' : Val -> Val -> M UnifyResult -- flex/flex - (_, VMeta fc k sp, VMeta fc' k' sp' ) => + unify' (VMeta fc k sp) (VMeta fc' k' sp') = if k == k' then unifySpine env mode (k == k') sp sp' -- TODO, might want to try the other way, too. else if length sp < length sp' then solve env k' sp' (VMeta fc k sp) >> pure neutral else solve env k sp (VMeta fc' k' sp') >> pure neutral - (_, t, VMeta fc' i' sp') => solve env i' sp' t >> pure neutral - (_, VMeta fc i sp, t' ) => solve env i sp t' >> pure neutral - (_, VPi fc _ _ a b, VPi fc' _ _ a' b') => do - let fresh = VVar fc l [<] + unify' t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral + unify' (VMeta fc i sp) t' = solve env i sp t' >> pure neutral + unify' (VPi fc _ _ a b) (VPi fc' _ _ a' b') = do + let fresh = VVar fc (length env) [<] [| unify env mode a a' <+> unify (fresh :: env) mode !(b $$ fresh) !(b' $$ fresh) |] - (_, VVar fc k sp, (VVar fc' k' sp') ) => + unify' t'@(VVar fc k sp) u'@(VVar fc' k' sp') = if k == k' then unifySpine env mode (k == k') sp sp' - else case (mode, sp, sp') of - (Pattern, [<],[<]) => if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] - _ => error fc "Failed to unify \{show t'} and \{show u'}" + else error fc "Failed to unify \{show t'} and \{show u'}" -- we don't eta expand on LHS - (Normal, VLam fc _ t, VLam _ _ t') => do - let fresh = VVar fc l [<] + unify' (VLam fc _ t) (VLam _ _ t') = do + let fresh = VVar fc (length env) [<] unify (fresh :: env) mode !(t $$ fresh) !(t' $$ fresh) - (Normal, t, VLam fc' _ t') => do + unify' t (VLam fc' _ t') = do debug "ETA \{show t}" - let fresh = VVar fc' l [<] + let fresh = VVar fc' (length env) [<] unify (fresh :: env) mode !(t `vapp` fresh) !(t' $$ fresh) - (Normal, VLam fc _ t, t' ) => do + unify' (VLam fc _ t) t' = do debug "ETA' \{show t'}" - let fresh = VVar fc l [<] + let fresh = VVar fc (length env) [<] unify (fresh :: env) mode !(t $$ fresh) !(t' `vapp` fresh) - -- We only want to do this for LHS pattern vars, otherwise, try expanding - (_, VVar fc k [<], u) => case mode of - Pattern => pure $ MkResult[(k, u)] - Normal => case !(tryEval env u) of + unify' t'@(VVar fc k [<]) u = case !(tryEval env u) of Just v => unify env mode t' v - Nothing => error fc "Failed to unify \{show t'} and \{show u'}" + Nothing => error fc "Failed to unify \{show t'} and \{show u}" - (_,t, VVar fc k [<]) => case mode of - Pattern => pure $ MkResult[(k, t)] - Normal => case !(tryEval env t) of + unify' t u'@(VVar fc k [<]) = case !(tryEval env t) of Just v => unify env mode v u' - Nothing => error fc "Failed to unify \{show t'} and \{show u'}" - - (_, VLam fc _ t, VLam _ _ t') => - let fresh = VVar fc l [<] in - unify (fresh :: env) mode !(t $$ fresh) !(t' $$ fresh) - (_, t, VLam fc' _ t') => do - debug "ETA \{show t}" - let fresh = VVar fc' l [<] - unify (fresh :: env) mode !(t `vapp` fresh) !(t' $$ fresh) - (_, VLam fc _ t, t' ) => do - debug "ETA' \{show t'}" - let fresh = VVar fc l [<] - unify (fresh :: env) mode !(t $$ fresh) !(t' `vapp` fresh) + Nothing => error fc "Failed to unify \{show t} and \{show u'}" -- REVIEW - consider separate value for DCon/TCon - (_, VRef fc k def sp, VRef fc' k' def' sp') => + unify' t'@(VRef fc k def sp) u'@(VRef fc' k' def' sp') = -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y do -- catchError {e = Error} (unifySpine env mode (k == k') sp sp') $ \ err => do @@ -317,23 +309,34 @@ unify env mode t u = do then unifySpine env mode (k == k') sp sp' else error fc "vref mismatch \{show t'} \{show u'}" - (_, VU _, VU _) => pure neutral + unify' (VU _) (VU _) = pure neutral -- Lennart.newt cursed type references itself -- We _could_ look up the ref, eval against [] and vappSpine... - (_, t, VRef fc' k' def sp') => do + unify' t u@(VRef fc' k' def sp') = do debug "expand \{show t} =?= %ref \{k'}" case lookup k' !(get) of Just (MkEntry name ty (Fn tm)) => unify env mode t !(vappSpine !(eval [] CBN tm) sp') - _ => error fc' "unify failed \{show t'} =?= \{show u'} [no Fn]\n env is \{show env}" + _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]\n env is \{show env}" - (_, VRef fc k def sp, u) => do + unify' t@(VRef fc k def sp) u = do debug "expand %ref \{k} \{show sp} =?= \{show u}" case lookup k !(get) of Just (MkEntry name ty (Fn tm)) => unify env mode !(vappSpine !(eval [] CBN tm) sp) u - _ => error fc "unify failed \{show t'} [no Fn] =?= \{show u'}\n env is \{show env}" + _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}\n env is \{show env}" -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. - _ => error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" + unify' t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" + + unifyPattern : Val -> Val -> M UnifyResult + unifyPattern t'@(VVar fc k sp) u'@(VVar fc' k' sp') = + if k == k' then unifySpine env mode (k == k') sp sp' + else case (sp, sp') of + ([<],[<]) => if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] + _ => error fc "Failed to unify \{show t'} and \{show u'}" + + unifyPattern (VVar fc k [<]) u = pure $ MkResult[(k, u)] + unifyPattern t (VVar fc k [<]) = pure $ MkResult [(k, t)] + unifyPattern t u = unify' t u export unifyCatch : FC -> Context -> Val -> Val -> M () diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index dba9abc..92fe5fd 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -366,6 +366,10 @@ parseDef = do pats <- many patAtom keyword "=" body <- typeExpr + w <- optional $ do + keyword "where" + startBlock $ manySame $ (parseSig <|> parseDef) + -- these get collected later pure $ Def fc nm [(t, body)] -- [MkClause fc [] t body] diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 8064bbb..f09d2bb 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -50,7 +50,6 @@ findMatches ctx ty ((MkEntry name type def) :: xs) = do debug "No match \{show ty} \{pprint [] type} \{showError "" err}" writeIORef top.metas mc findMatches ctx ty xs) -findMatches ctx ty (y :: xs) = findMatches ctx ty xs contextMatches : Context -> Val -> M (List (Tm, MetaContext)) contextMatches ctx ty = go (zip ctx.env (toList ctx.types))