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

add types to metas, find example that needs postpone

Browse Source
This commit is contained in:
Steve Dunham
2024-09-17 22:11:23 -07:00
parent 699a4bd575
commit 4f7b78f056
6 changed files with 65 additions and 31 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
newt/typeclass.newt
View File

@@ -39,3 +39,19 @@ MaybeMonad = MkMonad {Maybe} (\ {A} ma amb =>
bind : {m : U -> U} -> {x : Monad m} -> {a b : U} -> (m a) -> (a -> m b) -> m b
bind {m} {MkMonad bind'} = bind'
ptype Int
-- For now, we may try to solve this at creation time, but it's possible postpone is needed
/-
So I think we need to solve meta 7 first, and then if we're lucky, it's var 0 and we're
good to go.
failed to unify ( Maybe ( ?m:9 x:0 ) )
with ( ( ?m:4 x:0 ) ( ?m:7 x:0 ) )
non-variable in pattern (%meta 7 [< (%var 0 [< ])])
-/
foo : Int -> Maybe Int
foo x = bind {_} {_} (Just x) (\ x => Just x)

25
src/Lib/Check.idr
View File

@@ -22,7 +22,7 @@ data Pden = PR Nat Nat (List Nat)
forceMeta : Val -> M Val
forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
(Unsolved pos k xs) => pure (VMeta fc ix sp)
(Unsolved pos k xs _) => pure (VMeta fc ix sp)
(Solved k t) => vappSpine t sp >>= forceMeta
forceMeta x = pure x
@@ -33,7 +33,7 @@ forceType (VRef fc nm def sp) =
(Just (MkEntry name type (Fn t))) => vappSpine !(eval [] CBN t) sp
_ => pure (VRef fc nm def sp)
forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
(Unsolved x k xs) => pure (VMeta fc ix sp)
(Unsolved x k xs _) => pure (VMeta fc ix sp)
(Solved k t) => vappSpine t sp >>= forceType
forceType x = pure x
@@ -63,7 +63,7 @@ parameters (ctx: Context)
error fc "non-linear pattern"
else go xs (k :: acc)
go _ _ = error emptyFC "non-variable in pattern"
go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}"
-- we have to "lift" the renaming when we go under a lambda
-- I think that essentially means our domain ix are one bigger, since we're looking at lvl
@@ -221,7 +221,8 @@ insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
insert ctx tm ty = do
case !(forceMeta ty) of
VPi fc x Implicit a b => do
m <- freshMeta ctx (getFC tm)
m <- freshMeta ctx (getFC tm) a
debug "INSERT \{pprint (names ctx) m} : \{show a}"
mv <- eval ctx.env CBN m
insert ctx (App emptyFC tm m) !(b $$ mv)
va => pure (tm, va)
@@ -322,13 +323,17 @@ extendPi ctx ty nms sc = pure (ctx, ty, nms <>> [], sc)
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
updateContext ({env $= replace ix val, bds $= replace ix Defined } ctx) cs
updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs
where
replace : Nat -> a -> List a -> List a
replace k x [] = []
replace 0 x (y :: xs) = x :: xs
replace (S k) x (y :: xs) = y :: replace k x xs
replaceV : Nat -> a -> Vect n a -> Vect n a
replaceV k x [] = []
replaceV 0 x (y :: xs) = x :: xs
replaceV (S k) x (y :: xs) = y :: replaceV k x xs
-- ok, so this is a single constructor, CaseAlt
-- since we've gotten here, we assume it's possible and we better have at least
@@ -635,8 +640,8 @@ infer ctx (RApp fc t u icit) = do
-- TODO test case to cover this.
tty => do
debug "unify PI for \{show tty}"
a <- eval ctx.env CBN !(freshMeta ctx fc)
b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc
a <- eval ctx.env CBN !(freshMeta ctx fc (VU emptyFC))
b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC)
unifyCatch fc ctx tty (VPi fc ":ins" icit a b)
pure (a,b)
@@ -666,7 +671,7 @@ infer ctx (RAnn fc tm rty) = do
pure (tm, vty)
infer ctx (RLam fc nm icit tm) = do
a <- freshMeta ctx fc >>= eval ctx.env CBN
a <- freshMeta ctx fc (VU emptyFC) >>= eval ctx.env CBN
let ctx' = extend ctx nm a
(tm', b) <- infer ctx' tm
debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}"
@@ -674,9 +679,9 @@ infer ctx (RLam fc nm icit tm) = do
-- error {ctx} [DS "can't infer lambda"]
infer ctx (RImplicit fc) = do
ty <- freshMeta ctx fc
ty <- freshMeta ctx fc (VU emptyFC)
vty <- eval ctx.env CBN ty
tm <- freshMeta ctx fc
tm <- freshMeta ctx fc vty
pure (tm, vty)
infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String"))

3
src/Lib/CompileExp.idr
View File

@@ -79,7 +79,6 @@ compileTerm (Bnd _ k) = pure $ CBnd k
-- need to eta expand to arity
compileTerm t@(Ref fc nm _) = apply (CRef nm) [] [<] !(arityForName fc nm)
-- need to zonk
compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
compileTerm (Lam _ nm t) = pure $ CLam nm !(compileTerm t)
compileTerm tm@(App _ _ _) with (funArgs tm)
@@ -93,7 +92,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm)
-- apply (CRef "Meta\{show k}") args' [<] 0
arity <- case meta of
-- maybe throw
(Unsolved x j xs) => pure 0
(Unsolved x j ctx _) => pure 0 -- FIXME # of Bound in ctx.bds
(Solved j tm) => pure $ getArity !(quote 0 tm)
apply (CRef "Meta\{show k}") args' [<] arity
_ | (t@(Ref fc nm _), args) = do

6
src/Lib/ProcessDecl.idr
View File

@@ -76,9 +76,13 @@ processDecl (Def fc nm clauses) = do
tm' <- zonk ctx 0 [] tm
putStrLn "NF \{pprint[] tm'}"
mc <- readIORef ctx.metas
-- Maybe here we try search?
for_ mc.metas $ \case
(Solved k x) => pure ()
(Unsolved (l,c) k xs) => do
(Unsolved (l,c) k xs ty) => do
-- should just print, but it's too subtle in the sea of messages
-- we'd also need the ability to mark the whole top context as failure if we continue
-- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}"

32
src/Lib/TT.idr
View File

@@ -34,19 +34,25 @@ error' msg = throwError $ E (0,0) msg
-- because of dependent types (if we want something well-typed back out)
export
freshMeta : Context -> FC -> M Tm
freshMeta ctx fc = do
freshMeta : Context -> FC -> Val -> M Tm
freshMeta ctx fc ty = do
mc <- readIORef ctx.metas
putStrLn "INFO at \{show fc}: fresh meta \{show mc.next}"
writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx.bds ::) } mc
writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty ::) } mc
pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
where
-- hope I got the right order here :)
applyBDs : Nat -> Tm -> List BD -> Tm
applyBDs k t [] = t
-- review the order here
applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
-- hope I got the right order here :)
applyBDs : Nat -> Tm -> Vect k BD -> Tm
applyBDs k t [] = t
-- review the order here
applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
-- makeType : Vect k (String, Val) -> Vect k BD -> Val
-- makeType [] [] = ?makeType_rhs_2
-- makeType ((nm, ty) :: types) (Defined :: bds) = makeType types bds
-- makeType ((nm, ty) :: types) (Bound :: bds) = VPi emptyFC nm Explicit ty
export
lookupMeta : Nat -> M MetaEntry
@@ -57,7 +63,7 @@ lookupMeta ix = do
where
go : List MetaEntry -> M MetaEntry
go [] = error' "Meta \{show ix} not found"
go (meta@(Unsolved _ k ys) :: xs) = if k == ix then pure meta else go xs
go (meta@(Unsolved _ k ys _) :: xs) = if k == ix then pure meta else go xs
go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs
export partial
@@ -158,7 +164,7 @@ eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u)
eval env mode (U fc) = pure (VU fc)
eval env mode (Meta fc i) =
case !(lookupMeta i) of
(Unsolved _ k xs) => pure $ VMeta fc i [<]
(Unsolved _ k xs _) => pure $ VMeta fc i [<]
(Solved k t) => pure $ t
eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
@@ -221,7 +227,7 @@ solveMeta ctx ix tm = do
where
go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
go [] _ = error' "Meta \{show ix} not found"
go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix
go (meta@(Unsolved pos k _ _) :: xs) lhs = if k == ix
then do
-- empty context should be ok, because this needs to be closed
putStrLn "INFO at \{show pos}: solve \{show k} as \{!(prval tm)}"
@@ -267,7 +273,7 @@ zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
foo <- vappSpine v ([<] <>< sp')
debug "-> result is \{show foo}"
quote l foo
(Unsolved x j xs) => pure $ appSpine t sp
(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

14
src/Lib/Types.idr
View File

@@ -164,9 +164,9 @@ pprint names tm = render 80 $ go names tm
go names (App _ t u) = text "(" <+> go names t <+> go names u <+> ")"
go names (U _) = "U"
go names (Pi _ nm Implicit t u) =
text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "=>" <+> go (nm :: names) u <+> ")"
text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "->" <+> go (nm :: names) u <+> ")"
go names (Pi _ nm Explicit t u) =
text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")"
text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "->" <+> go (nm :: names) u <+> ")"
-- FIXME - probably way wrong on the names here. There is implicit binding going on
go names (Case _ sc alts) = text "case" <+> go names sc <+> text "of" </> (nest 2 (line ++ stack (map (goAlt names) alts)))
go names (Lit _ lit) = text "\{show lit}"
@@ -237,6 +237,8 @@ Show Val where
-- Not used - I was going to change context to have a List Binder
-- instead of env, types, bds
-- But when we get down into eval, we don't have types to put into the env
-- It looks like Idris has a separate LocalEnv in eval, Kovacs peels off
-- env from context and extends it.
data Binder : Type where
Bind : (nm : String) -> (bd : BD) -> (val : Val) -> (ty : Val) -> Binder
@@ -285,13 +287,15 @@ Can I get val back? Do we need to quote? What happens if we don't?
-}
record Context
public export
data MetaEntry = Unsolved FC Nat (List BD) | Solved Nat Val
data MetaEntry = Unsolved FC Nat Context Val | Solved Nat Val
export
covering
Show MetaEntry where
show (Unsolved pos k xs) = "Unsolved \{show pos} \{show k}"
show (Unsolved pos k xs ty) = "Unsolved \{show pos} \{show k} : \{show ty}"
show (Solved k x) = "Solved \{show k} \{show x}"
public export
@@ -356,7 +360,7 @@ record Context where
env : Env -- Values in scope
types : Vect lvl (String, Val) -- types and names in scope
-- so we'll try "bds" determines length of local context
bds : List BD -- bound or defined
bds : Vect lvl BD -- bound or defined
-- We only need this here if we don't pass TopContext
-- top : TopContext