dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

pattern matching can dot with applied vars

Browse Source
This commit is contained in:
Steve Dunham
2025-12-29 09:51:30 -08:00
parent 3abd18ce48
commit 223b1563a9
1 changed files with 6 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
src/Lib/Elab.newt
View File

@@ -98,6 +98,9 @@ instance Monoid UnifyResult where
neutral = MkResult Nil neutral = MkResult Nil
data UnifyMode = UNormal | UPattern data UnifyMode = UNormal | UPattern
instance Show UnifyMode where
show UNormal = "UNormal"
show UPattern = "UPattern"
check : Context -> Raw -> Val -> M Tm check : Context -> Raw -> Val -> M Tm
@@ -581,7 +584,9 @@ unify env mode t u = do
(Lin,Lin) => if k < k' (Lin,Lin) => if k < k'
then pure $ MkResult ((k, u') :: Nil) then pure $ MkResult ((k, u') :: Nil)
else pure $ MkResult ((k', t') :: Nil) else pure $ MkResult ((k', t') :: Nil)
_ => error fc "Failed to unify \{show t'} and \{show u'}" (Lin,_) => pure $ MkResult ((k, u') :: Nil)
(_,Lin) => pure $ MkResult ((k', t') :: Nil)
_ => error fc "Failed to unify \{show t'} and \{show u'} at \{show mode}"
unifyPattern (VVar fc k Lin) u = pure $ MkResult((k, u) :: Nil) unifyPattern (VVar fc k Lin) u = pure $ MkResult((k, u) :: Nil)
unifyPattern t (VVar fc k Lin) = pure $ MkResult ((k, t) :: Nil) unifyPattern t (VVar fc k Lin) = pure $ MkResult ((k, t) :: Nil)