1509 lines
58 KiB
Agda
1509 lines
58 KiB
Agda
module Lib.Elab
|
||
|
||
import Lib.Parser.Impl
|
||
import Lib.Prettier
|
||
import Data.List
|
||
import Data.String
|
||
import Data.IORef
|
||
import Lib.Types
|
||
import Lib.Eval
|
||
import Lib.TopContext
|
||
import Lib.Syntax
|
||
|
||
|
||
vprint : Context -> Val -> M String
|
||
vprint ctx v = do
|
||
tm <- quote (length' ctx.env) v
|
||
pure $ render 90 $ pprint (names ctx) tm
|
||
|
||
|
||
-- collectDecl collects multiple Def for one function into one
|
||
|
||
collectDecl : List Decl -> List Decl
|
||
collectDecl Nil = Nil
|
||
collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
|
||
if nm == nm' then collectDecl (Def fc nm (cl ++ cl') :: xs)
|
||
else (Def fc nm cl :: collectDecl rest)
|
||
collectDecl (x :: xs) = x :: collectDecl xs
|
||
|
||
rpprint : List String → Tm → String
|
||
rpprint names tm = render 90 $ pprint names tm
|
||
|
||
-- renaming
|
||
-- dom gamma ren
|
||
data Pden = PR Int Int (List Int)
|
||
|
||
showCtx : Context -> M String
|
||
showCtx ctx =
|
||
unlines ∘ reverse <$> go (names ctx) 0 (reverse $ zip ctx.env ctx.types) Nil
|
||
where
|
||
isVar : Int -> Val -> Bool
|
||
isVar k (VVar _ k' Lin) = k == k'
|
||
isVar _ _ = False
|
||
|
||
go : List String -> Int -> List (Val × String × Val) -> List String -> M (List String)
|
||
go _ _ Nil acc = pure acc
|
||
go names k ((v, n, ty) :: xs) acc = if isVar k v
|
||
-- TODO - use Doc and add <+/> as appropriate to printing
|
||
then do
|
||
tty <- quote ctx.lvl ty
|
||
go names (1 + k) xs (" \{n} : \{rpprint names tty}" :: acc)
|
||
else do
|
||
tm <- quote ctx.lvl v
|
||
tty <- quote ctx.lvl ty
|
||
go names (1 + k) xs (" \{n} = \{rpprint names tm} : \{rpprint names tty}" :: acc)
|
||
|
||
dumpCtx : Context -> M String
|
||
dumpCtx ctx = do
|
||
let names = (map fst ctx.types)
|
||
-- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
|
||
env <- for (zip ctx.env ctx.types) $ \case
|
||
(v, n, ty) => do
|
||
sty <- vprint ctx ty
|
||
sv <- vprint ctx v
|
||
pure " \{n} : \{sty} = \{sv}"
|
||
let msg = unlines (reverse env) -- ++ " -----------\n" ++ " goal \{rpprint names ty'}"
|
||
pure msg
|
||
|
||
|
||
|
||
-- return Bnd and type for name
|
||
|
||
lookupName : Context -> String -> Maybe (Tm × Val)
|
||
lookupName ctx name = go 0 ctx.types
|
||
where
|
||
go : Int -> List (String × Val) -> Maybe (Tm × Val)
|
||
go ix Nil = Nothing
|
||
-- FIXME - we should stuff a Binder of some sort into "types"
|
||
go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (1 + ix) xs
|
||
|
||
|
||
lookupDef : Context -> String -> Maybe Val
|
||
lookupDef ctx name = go 0 ctx.types ctx.env
|
||
where
|
||
go : Int -> List (String × Val) -> List Val -> Maybe Val
|
||
go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs
|
||
go ix _ _ = Nothing
|
||
|
||
|
||
-- IORef for metas needs IO
|
||
|
||
forceMeta : Val -> M Val
|
||
forceMeta (VMeta fc ix sp) = do
|
||
meta <- lookupMeta ix
|
||
case meta of
|
||
(Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp)
|
||
(Solved _ k t) => vappSpine t sp >>= forceMeta
|
||
forceMeta x = pure x
|
||
|
||
|
||
record UnifyResult where
|
||
constructor MkResult
|
||
-- wild guess here - lhs is a VVar
|
||
constraints : List (Int × Val)
|
||
|
||
instance Semigroup UnifyResult where
|
||
(MkResult cs) <+> (MkResult cs') = MkResult (cs ++ cs')
|
||
|
||
instance Monoid UnifyResult where
|
||
neutral = MkResult Nil
|
||
|
||
data UnifyMode = UNormal | UPattern
|
||
|
||
|
||
|
||
check : Context -> Raw -> Val -> M Tm
|
||
|
||
|
||
unifyCatch : FC -> Context -> Val -> Val -> M Unit
|
||
|
||
-- Check that the arguments are not explicit and the type constructor in codomain matches
|
||
-- Later we will build a table of codomain type, and maybe make the user tag the candidates
|
||
-- like Idris does with %hint
|
||
isCandidate : Val -> Tm -> Bool
|
||
isCandidate ty (Pi fc nm Explicit rig t u) = False
|
||
isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u
|
||
isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm'
|
||
isCandidate ty (App fc t u) = isCandidate ty t
|
||
isCandidate _ _ = False
|
||
|
||
-- This is a crude first pass
|
||
|
||
findMatches : Context -> Val -> List TopEntry -> M (List String)
|
||
findMatches ctx ty Nil = pure Nil
|
||
findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
|
||
let (True) = isCandidate ty type | False => findMatches ctx ty xs
|
||
top <- get
|
||
-- let ctx = mkCtx (getFC ty)
|
||
-- FIXME we're restoring state, but the INFO logs have already been emitted
|
||
-- Also redo this whole thing to run during elab, recheck constraints, etc.
|
||
mc <- readIORef top.metaCtx
|
||
catchError(do
|
||
-- TODO sort out the FC here
|
||
let fc = getFC ty
|
||
debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}"
|
||
-- This check is solving metas, so we save mc below in case we want this solution
|
||
-- tm <- check (mkCtx fc) (RVar fc name) ty
|
||
-- FIXME RVar should optionally have qualified names
|
||
let (QN ns nm) = name
|
||
tm <- check ctx (RVar fc nm) ty
|
||
debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
|
||
writeIORef top.metaCtx mc
|
||
(_::_ nm) <$> findMatches ctx ty xs)
|
||
(\ err => do
|
||
debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}"
|
||
writeIORef top.metaCtx mc
|
||
findMatches ctx ty xs)
|
||
|
||
|
||
contextMatches : Context -> Val -> M (List (Tm × Val))
|
||
contextMatches ctx ty = go (zip ctx.env ctx.types)
|
||
where
|
||
go : List (Val × String × Val) -> M (List (Tm × Val))
|
||
go Nil = pure Nil
|
||
go ((tm, nm, vty) :: xs) = do
|
||
type <- quote ctx.lvl vty
|
||
let (True) = isCandidate ty type | False => go xs
|
||
top <- get
|
||
mc <- readIORef top.metaCtx
|
||
catchError(do
|
||
debug $ \ _ => "TRY context \{nm} : \{rpprint (names ctx) type} for \{show ty}"
|
||
unifyCatch (getFC ty) ctx ty vty
|
||
mc' <- readIORef top.metaCtx
|
||
writeIORef top.metaCtx mc
|
||
tm <- quote ctx.lvl tm
|
||
(_::_ (tm, vty)) <$> go xs)
|
||
(\ err => do
|
||
debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}"
|
||
writeIORef top.metaCtx mc
|
||
go xs)
|
||
|
||
|
||
getArity : Tm -> Int
|
||
getArity (Pi x str icit rig t u) = 1 + getArity u
|
||
-- Ref or App (of type constructor) are valid
|
||
getArity _ = 0
|
||
|
||
-- Can metas live in context for now?
|
||
-- We'll have to be able to add them, which might put gamma in a ref
|
||
|
||
|
||
|
||
-- Makes the arg for `solve` when we solve an auto
|
||
makeSpine : Int -> List BD -> SnocList Val
|
||
makeSpine k Nil = Lin
|
||
makeSpine k (Defined :: xs) = makeSpine (k - 1) xs
|
||
makeSpine k (Bound :: xs) = makeSpine (k - 1) xs :< VVar emptyFC (k - 1) Lin
|
||
|
||
|
||
solve : Env -> (k : Int) -> SnocList Val -> Val -> M Unit
|
||
|
||
|
||
|
||
trySolveAuto : MetaEntry -> M Bool
|
||
trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
|
||
debug $ \ _ => "TRYAUTO solving \{show k} : \{show ty}"
|
||
-- fill in solved metas in type
|
||
x <- quote ctx.lvl ty
|
||
ty <- eval ctx.env CBN x
|
||
debug $ \ _ => "AUTO ---> \{show ty}"
|
||
-- we want the context here too.
|
||
top <- get
|
||
Nil <- contextMatches ctx ty
|
||
| ((tm, vty) :: Nil) => do
|
||
unifyCatch (getFC ty) ctx ty vty
|
||
val <- eval ctx.env CBN tm
|
||
debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
|
||
let sp = makeSpine ctx.lvl ctx.bds
|
||
solve ctx.env k sp val
|
||
pure True
|
||
| res => do
|
||
debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
|
||
pure False
|
||
(nm :: Nil) <- findMatches ctx ty $ map snd $ toList top.defs
|
||
| res => do
|
||
debug $ \ _ => "FAILED to solve \{show ty}, matches: \{show res}"
|
||
pure False
|
||
tm <- check ctx (RVar fc nm) ty
|
||
val <- eval ctx.env CBN tm
|
||
debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
|
||
let sp = makeSpine ctx.lvl ctx.bds
|
||
solve ctx.env k sp val
|
||
pure True
|
||
trySolveAuto _ = pure False
|
||
|
||
-- export
|
||
-- solveAutos : Int -> List MetaEntry -> M Unit
|
||
-- solveAutos mstart Nil = pure MkUnit
|
||
-- solveAutos mstart (entry :: es) = do
|
||
-- res <- trySolveAuto entry
|
||
-- -- idris is inlining this and blowing stack?
|
||
-- if res
|
||
-- then do
|
||
-- top <- get
|
||
-- mc <- readIORef top.metaCtx
|
||
-- let mlen = length mc.metas `minus` mstart
|
||
-- solveAutos mstart (take mlen mc.metas)
|
||
-- else
|
||
-- solveAutos mstart es
|
||
|
||
|
||
-- Called from ProcessDecl, this was popping the stack, the tail call optimization doesn't
|
||
-- handle the traversal of the entire meta list. I've turned the restart into a trampoline
|
||
-- and filtered it down to unsolved autos.
|
||
|
||
solveAutos : Int -> M Unit
|
||
solveAutos mstart = do
|
||
top <- get
|
||
mc <- readIORef top.metaCtx
|
||
let mlen = length' mc.metas - mstart
|
||
res <- run $ filter isAuto (ite (mstart == 0) mc.metas $ take (cast mlen) mc.metas)
|
||
if res then solveAutos mstart else pure MkUnit
|
||
where
|
||
isAuto : MetaEntry -> Bool
|
||
isAuto (Unsolved fc k ctx x AutoSolve xs) = True
|
||
isAuto _ = False
|
||
|
||
run : List MetaEntry -> M Bool
|
||
run Nil = pure False
|
||
run (e :: es) = do
|
||
res <- trySolveAuto e
|
||
if res then pure True else run es
|
||
|
||
-- We need to switch to SortedMap here
|
||
|
||
updateMeta : Int -> (MetaEntry -> M MetaEntry) -> M Unit
|
||
updateMeta ix f = do
|
||
top <- get
|
||
mc <- readIORef top.metaCtx
|
||
metas <- go mc.metas
|
||
writeIORef top.metaCtx $ MC metas mc.next
|
||
where
|
||
go : List MetaEntry -> M (List MetaEntry)
|
||
go Nil = error' "Meta \{show ix} not found"
|
||
go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs
|
||
go (x@((Solved _ k y)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs
|
||
|
||
|
||
checkAutos : Int -> List MetaEntry -> M Unit
|
||
checkAutos ix Nil = pure MkUnit
|
||
checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
|
||
ty' <- quote ctx.lvl ty
|
||
when (usesMeta ty') $ \ _ => ignore $ trySolveAuto entry
|
||
checkAutos ix rest
|
||
where
|
||
usesMeta : Tm -> Bool
|
||
usesMeta (App _ (Meta _ k) u) = if k == ix then True else usesMeta u
|
||
usesMeta (App _ _ u) = usesMeta u
|
||
usesMeta _ = False
|
||
checkAutos ix (_ :: rest) = checkAutos ix rest
|
||
|
||
|
||
|
||
addConstraint : Env -> Int -> SnocList Val -> Val -> M Unit
|
||
addConstraint env ix sp tm = do
|
||
updateMeta ix $ \case
|
||
(Unsolved pos k a b c cons) => do
|
||
debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
|
||
pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
|
||
(Solved _ k tm) => error' "Meta \{show k} already solved (addConstraint :: Nil)"
|
||
top <- get
|
||
mc <- readIORef top.metaCtx
|
||
checkAutos ix mc.metas
|
||
-- this loops too
|
||
-- solveAutos 0 mc.metas
|
||
pure MkUnit
|
||
|
||
|
||
-- return renaming, the position is the new VVar
|
||
invert : Int -> SnocList Val -> M (List Int)
|
||
invert lvl sp = go sp Nil
|
||
where
|
||
go : SnocList Val -> List Int -> M (List Int)
|
||
go Lin acc = pure $ reverse acc
|
||
go (xs :< VVar fc k Lin) acc = do
|
||
if elem k acc
|
||
then do
|
||
debug $ \ _ => "\{show k} \{show acc}"
|
||
-- when does this happen?
|
||
error fc "non-linear pattern: \{show sp}"
|
||
else go xs (k :: acc)
|
||
go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}"
|
||
|
||
|
||
-- REVIEW why am I converting to Tm?
|
||
-- 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
|
||
-- in the codomain, so maybe we can just keep that value
|
||
|
||
rename : Int -> List Int -> Int -> Val -> M Tm
|
||
|
||
renameSpine : Int -> List Int -> Int -> Tm -> SnocList Val -> M Tm
|
||
renameSpine meta ren lvl tm Lin = pure tm
|
||
renameSpine meta ren lvl tm (xs :< x) = do
|
||
xtm <- rename meta ren lvl x
|
||
xs' <- renameSpine meta ren lvl tm xs
|
||
pure $ App emptyFC xs' xtm
|
||
|
||
rename meta ren lvl (VVar fc k sp) = case findIndex' (_==_ k) ren of
|
||
Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}"
|
||
Just x => renameSpine meta ren lvl (Bnd fc x) sp
|
||
rename meta ren lvl (VRef fc nm def sp) = renameSpine meta ren lvl (Ref fc nm def) sp
|
||
rename meta ren lvl (VMeta fc ix sp) = do
|
||
-- So sometimes we have an unsolved meta in here which reference vars out of scope.
|
||
debug $ \ _ => "rename Meta \{show ix} spine \{show sp}"
|
||
if ix == meta
|
||
-- REVIEW is this the right fc?
|
||
then error fc "meta occurs check"
|
||
else do
|
||
meta' <- lookupMeta ix
|
||
case meta' of
|
||
Solved fc _ val => do
|
||
debug $ \ _ => "rename: \{show ix} is solved"
|
||
val' <- vappSpine val sp
|
||
rename meta ren lvl val'
|
||
_ => do
|
||
debug $ \ _ => "rename: \{show ix} is unsolved"
|
||
catchError (renameSpine meta ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err))
|
||
rename meta ren lvl (VLam fc n icit rig t) = do
|
||
tapp <- t $$ VVar fc lvl Lin
|
||
scope <- rename meta (lvl :: ren) (1 + lvl) tapp
|
||
pure (Lam fc n icit rig scope)
|
||
rename meta ren lvl (VPi fc n icit rig ty tm) = do
|
||
ty' <- rename meta ren lvl ty
|
||
tmapp <- tm $$ VVar emptyFC lvl Lin
|
||
scope' <- rename meta (lvl :: ren) (1 + lvl) tmapp
|
||
pure (Pi fc n icit rig ty' scope')
|
||
rename meta ren lvl (VU fc) = pure (UU fc)
|
||
rename meta ren lvl (VErased fc) = pure (Erased fc)
|
||
-- for now, we don't do solutions with case in them.
|
||
rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution"
|
||
rename meta ren lvl (VLit fc lit) = pure (Lit fc lit)
|
||
rename meta ren lvl (VLet fc name val body) = do
|
||
val' <- rename meta ren lvl val
|
||
body' <- rename meta (lvl :: ren) (1 + lvl) body
|
||
pure $ Let fc name val' body'
|
||
-- these probably shouldn't show up in solutions...
|
||
rename meta ren lvl (VLetRec fc name ty val body) = do
|
||
ty' <- rename meta ren lvl ty
|
||
val' <- rename meta (lvl :: ren) (1 + lvl) val
|
||
body' <- rename meta (lvl :: ren) (1 + lvl) body
|
||
pure $ LetRec fc name ty' val' body'
|
||
|
||
lams : Nat -> List String -> Tm -> Tm
|
||
lams Z _ tm = tm
|
||
-- REVIEW do we want a better FC, icity?, rig?
|
||
lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm)
|
||
lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm)
|
||
|
||
|
||
unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult
|
||
|
||
.boundNames : Context -> List String
|
||
ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst ctx.types)
|
||
|
||
solve env m sp t = do
|
||
meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m
|
||
| _ => error (getFC t) "Meta \{show m} already solved! (solve :: Nil)"
|
||
debug $ \ _ => "SOLVE \{show m} \{show kind} lvl \{show $ length' env} sp \{show sp} is \{show t}"
|
||
let size = length $ filter (\x => x == Bound) ctx_.bds
|
||
debug $ \ _ => "\{show m} size is \{show size} sps \{show $ snoclen sp}"
|
||
let (True) = snoclen sp == size
|
||
| _ => do
|
||
let l = length' env
|
||
debug $ \ _ => "meta \{show m} (\{show ix}) applied to \{show $ snoclen sp} args instead of \{show size}"
|
||
debug $ \ _ => "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}"
|
||
addConstraint env m sp t
|
||
let l = length' env
|
||
debug $ \ _ => "meta \{show meta}"
|
||
ren <- invert l sp
|
||
-- force unlet
|
||
hack <- quote l t
|
||
t <- eval env CBN hack
|
||
catchError (do
|
||
tm <- rename m ren l t
|
||
|
||
let tm = lams (snoclen sp) (reverse ctx_.boundNames) tm
|
||
top <- get
|
||
soln <- eval Nil CBN tm
|
||
|
||
updateMeta m $ \case
|
||
(Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
|
||
(Solved _ k x) => error' "Meta \{show ix} already solved! (solve2 :: Nil)"
|
||
for cons $ \case
|
||
MkMc fc env sp rhs => do
|
||
val <- vappSpine soln sp
|
||
debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}"
|
||
unify env UNormal val rhs
|
||
mc <- readIORef top.metaCtx
|
||
-- stack ...
|
||
-- checkAutos ix mc.metas
|
||
pure MkUnit
|
||
)
|
||
|
||
(\case
|
||
Postpone fc ix msg => do
|
||
-- let someone else solve this and then check again.
|
||
debug $ \ _ => "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}"
|
||
addConstraint env m sp t
|
||
-- I get legit errors after stuffing in solution
|
||
-- report for now, tests aren't hitting this branch
|
||
err => throwError err
|
||
-- debug $ \ _ => "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}"
|
||
-- debug $ \ _ => "because \{showError "" err}"
|
||
-- addConstraint env m sp t
|
||
)
|
||
|
||
unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult
|
||
unifySpine env mode False _ _ = error emptyFC "unify failed at head" -- unreachable now
|
||
unifySpine env mode True Lin Lin = pure (MkResult Nil)
|
||
unifySpine env mode True (xs :< x) (ys :< y) =
|
||
-- I had idiom brackets here, technically fairly easy to desugar, but not adding at this time
|
||
_<+>_ <$> 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}"
|
||
debug $ \ _ => " =?= \{show u}"
|
||
t' <- forceMeta t >>= unlet env
|
||
u' <- forceMeta u >>= unlet env
|
||
debug $ \ _ => "forced \{show t'}"
|
||
debug $ \ _ => " =?= \{show u'}"
|
||
debug $ \ _ => "env \{show env}"
|
||
-- debug $ \ _ => "types \{show $ ctx.types}"
|
||
let l = length' env
|
||
-- 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
|
||
UPattern => unifyPattern t' u'
|
||
UNormal => unifyMeta t' u'
|
||
|
||
-- The case tree is still big here. It's hard for idris to sort
|
||
-- What we really want is what I wrote - handle meta, handle lam, handle var, etc
|
||
|
||
where
|
||
-- The case tree here was huge, so I split it into stages
|
||
-- newt will have similar issues because it doesn't emit a default case
|
||
|
||
unifyRest : Val -> Val -> M UnifyResult
|
||
unifyRest (VPi fc _ _ _ a b) (VPi fc' _ _ _ a' b') = do
|
||
let fresh = VVar fc (length' env) Lin
|
||
xb <- b $$ fresh
|
||
xb' <- b' $$ fresh
|
||
_<+>_ <$> unify env mode a a' <*> unify (fresh :: env) mode xb xb'
|
||
|
||
unifyRest (VU _) (VU _) = pure neutral
|
||
-- REVIEW I'd like to quote this back, but we have l that aren't in the environment.
|
||
unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}"
|
||
|
||
unifyRef : Val -> Val -> M UnifyResult
|
||
unifyRef 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(unifySpine env mode (k == k') sp sp') $ \ err => do
|
||
Nothing <- tryEval env t'
|
||
| Just v => do
|
||
debug $ \ _ => "tryEval \{show t'} to \{show v}"
|
||
unify env mode v u'
|
||
Nothing <- tryEval env u'
|
||
| Just v => unify env mode t' v
|
||
if k == k'
|
||
then unifySpine env mode (k == k') sp sp'
|
||
else error fc "vref mismatch \{show t'} \{show u'}"
|
||
|
||
-- Lennart.newt cursed type references itself
|
||
-- We _could_ look up the ref, eval against Nil and vappSpine...
|
||
unifyRef t u@(VRef fc' k' def sp') = do
|
||
debug $ \ _ => "expand \{show t} =?= %ref \{show k'}"
|
||
top <- get
|
||
case lookup k' top of
|
||
Just (MkEntry _ name ty (Fn tm)) => do
|
||
vtm <- eval Nil CBN tm
|
||
appvtm <- vappSpine vtm sp'
|
||
unify env mode t appvtm
|
||
_ => error fc' "unify failed \{show t} =?= \{show u} (no Fn :: Nil)\n env is \{show env}"
|
||
|
||
unifyRef t@(VRef fc k def sp) u = do
|
||
debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
|
||
top <- get
|
||
case lookup k top of
|
||
Just (MkEntry _ name ty (Fn tm)) => do
|
||
vtm <- eval Nil CBN tm
|
||
tmsp <- vappSpine vtm sp
|
||
unify env mode tmsp u
|
||
_ => error fc "unify failed \{show t} (no Fn :: Nil) =?= \{show u}\n env is \{show env}"
|
||
unifyRef t u = unifyRest t u
|
||
|
||
unifyVar : Val -> Val -> M UnifyResult
|
||
unifyVar t'@(VVar fc k sp) u'@(VVar fc' k' sp') =
|
||
if k == k' then unifySpine env mode (k == k') sp sp'
|
||
else error fc "Failed to unify \{show t'} and \{show u'}"
|
||
|
||
unifyVar t'@(VVar fc k Lin) u = do
|
||
vu <- tryEval env u
|
||
case vu of
|
||
Just v => unify env mode t' v
|
||
Nothing => error fc "Failed to unify \{show t'} and \{show u}"
|
||
|
||
unifyVar t u'@(VVar fc k Lin) = do
|
||
vt <- tryEval env t
|
||
case vt of
|
||
Just v => unify env mode v u'
|
||
Nothing => error fc "Failed to unify \{show t} and \{show u'}"
|
||
unifyVar t u = unifyRef t u
|
||
|
||
unifyLam : Val -> Val -> M UnifyResult
|
||
unifyLam (VLam fc _ _ _ t) (VLam _ _ _ _ t') = do
|
||
let fresh = VVar fc (length' env) Lin
|
||
vappt <- t $$ fresh
|
||
vappt' <- t' $$ fresh
|
||
unify (fresh :: env) mode vappt vappt'
|
||
unifyLam t (VLam fc' _ _ _ t') = do
|
||
debug $ \ _ => "ETA \{show t}"
|
||
let fresh = VVar fc' (length' env) Lin
|
||
vappt <- vapp t fresh
|
||
vappt' <- t' $$ fresh
|
||
unify (fresh :: env) mode vappt vappt'
|
||
unifyLam (VLam fc _ _ _ t) t' = do
|
||
debug $ \ _ => "ETA' \{show t'}"
|
||
let fresh = VVar fc (length' env) Lin
|
||
appt <- t $$ fresh
|
||
vappt' <- vapp t' fresh
|
||
unify (fresh :: env) mode appt vappt'
|
||
unifyLam t u = unifyVar t u
|
||
|
||
unifyMeta : Val -> Val -> M UnifyResult
|
||
-- flex/flex
|
||
unifyMeta (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 snoclen sp < snoclen sp'
|
||
then solve env k' sp' (VMeta fc k sp) >> pure neutral
|
||
else solve env k sp (VMeta fc' k' sp') >> pure neutral
|
||
unifyMeta t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral
|
||
unifyMeta (VMeta fc i sp) t' = solve env i sp t' >> pure neutral
|
||
unifyMeta t v = unifyLam t v
|
||
|
||
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
|
||
(Lin,Lin) => if k < k'
|
||
then pure $ MkResult ((k, u') :: Nil)
|
||
else pure $ MkResult ((k', t') :: Nil)
|
||
_ => error fc "Failed to unify \{show t'} and \{show u'}"
|
||
|
||
unifyPattern (VVar fc k Lin) u = pure $ MkResult((k, u) :: Nil)
|
||
unifyPattern t (VVar fc k Lin) = pure $ MkResult ((k, t) :: Nil)
|
||
unifyPattern t u = unifyMeta t u
|
||
|
||
|
||
unifyCatch fc ctx ty' ty = do
|
||
res <- catchError (unify ctx.env UNormal ty' ty) $ \err => do
|
||
let names = map fst ctx.types
|
||
debug $ \ _ => "fail \{show ty'} \{show ty}"
|
||
a <- quote ctx.lvl ty'
|
||
b <- quote ctx.lvl ty
|
||
let msg = "unification failure: \{errorMsg err}\n failed to unify \{rpprint names a}\n with \{rpprint names b}\n "
|
||
throwError (E fc msg)
|
||
case res of
|
||
MkResult Nil => pure MkUnit
|
||
cs => do
|
||
-- probably want a unification mode that throws instead of returning constraints
|
||
-- TODO need a normalizeHoles, maybe on quote?
|
||
debug $ \ _ => "fail with constraints \{show cs.constraints}"
|
||
a <- quote ctx.lvl ty'
|
||
b <- quote ctx.lvl ty
|
||
let names = map fst ctx.types
|
||
let msg = "unification failure\n failed to unify \{rpprint names a}\n with \{rpprint names b}"
|
||
let msg = msg ++ "\nconstraints \{show cs.constraints}"
|
||
throwError (E fc msg)
|
||
-- error fc "Unification yields constraints \{show cs.constraints}"
|
||
|
||
|
||
freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
|
||
freshMeta ctx fc ty kind = do
|
||
top <- get
|
||
mc <- readIORef top.metaCtx
|
||
debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
|
||
let newmeta = Unsolved fc mc.next ctx ty kind Nil
|
||
writeIORef top.metaCtx $ MC (newmeta :: mc.metas) (1 + mc.next)
|
||
-- infinite loop - keeps trying Ord a => Ord (a \x a)
|
||
-- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta
|
||
pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
|
||
where
|
||
-- hope I got the right order here :)
|
||
applyBDs : Int -> Tm -> List BD -> Tm
|
||
applyBDs k t Nil = t
|
||
-- review the order here
|
||
applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k)
|
||
applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs
|
||
|
||
insert : (ctx : Context) -> Tm -> Val -> M (Tm × Val)
|
||
insert ctx tm ty = do
|
||
ty' <- forceMeta ty
|
||
case ty' of
|
||
VPi fc x Auto rig a b => do
|
||
m <- freshMeta ctx (getFC tm) a AutoSolve
|
||
debug $ \ _ => "INSERT Auto \{rpprint (names ctx) m} : \{show a}"
|
||
debug $ \ _ => "TM \{rpprint (names ctx) tm}"
|
||
mv <- eval ctx.env CBN m
|
||
bapp <- b $$ mv
|
||
insert ctx (App (getFC tm) tm m) bapp
|
||
VPi fc x Implicit rig a b => do
|
||
m <- freshMeta ctx (getFC tm) a Normal
|
||
debug $ \ _ => "INSERT \{rpprint (names ctx) m} : \{show a}"
|
||
debug $ \ _ => "TM \{rpprint (names ctx) tm}"
|
||
mv <- eval ctx.env CBN m
|
||
bapp <- b $$ mv
|
||
insert ctx (App (getFC tm) tm m) bapp
|
||
va => pure (tm, va)
|
||
|
||
primType : FC -> QName -> M Val
|
||
primType fc nm = do
|
||
top <- get
|
||
case lookup nm top of
|
||
Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name PrimTCon Lin
|
||
_ => error fc "Primitive type \{show nm} not in scope"
|
||
|
||
|
||
infer : Context -> Raw -> M (Tm × Val)
|
||
|
||
|
||
data Bind = MkBind String Icit Val
|
||
|
||
instance Show Bind where
|
||
show (MkBind str icit x) = "\{str} \{show icit}"
|
||
|
||
|
||
---------------- Case builder
|
||
|
||
|
||
record Problem where
|
||
constructor MkProb
|
||
clauses : List Clause
|
||
-- I think a pi-type representing the pattern args -> goal, so we're checking
|
||
-- We might pull out the pattern abstraction to a separate step and drop pats from clauses.
|
||
ty : Val
|
||
|
||
-- Might have to move this if Check reaches back in...
|
||
-- this is kinda sketchy, we can't use it twice at the same depth with the same name.
|
||
fresh : {{ctx : Context}} -> String -> String
|
||
fresh {{ctx}} base = base ++ "$" ++ show (length' ctx.env)
|
||
|
||
-- The result is a casetree, but it's in Tm
|
||
|
||
buildTree : Context -> Problem -> M Tm
|
||
|
||
-- Updates a clause for INTRO
|
||
introClause : String -> Icit -> Clause -> M Clause
|
||
introClause nm icit (MkClause fc cons (pat :: pats) expr) =
|
||
if icit == getIcit pat then pure $ MkClause fc ((nm, pat) :: cons) pats expr
|
||
else if icit == Implicit then pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) (pat :: pats) expr
|
||
else if icit == Auto then pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) (pat :: pats) expr
|
||
else error fc "Explicit arg and \{show $ getIcit pat} pattern \{show nm} \{show pat}"
|
||
-- handle implicts at end?
|
||
introClause nm Implicit (MkClause fc cons Nil expr) = pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) Nil expr
|
||
introClause nm Auto (MkClause fc cons Nil expr) = pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) Nil expr
|
||
introClause nm icit (MkClause fc cons Nil expr) = error fc "Clause size doesn't match"
|
||
|
||
-- A split candidate looks like x /? Con ...
|
||
-- we need a type here. I pulled if off of the
|
||
-- pi-type, but do we need metas solved or dependents split?
|
||
-- this may dot into a dependent.
|
||
findSplit : List Constraint -> Maybe Constraint
|
||
findSplit Nil = Nothing
|
||
-- FIXME look up type, ensure it's a constructor
|
||
findSplit (x@(nm, PatCon _ _ _ _ _) :: xs) = Just x
|
||
findSplit (x@(nm, PatLit _ val) :: xs) = Just x
|
||
findSplit (x :: xs) = findSplit xs
|
||
|
||
|
||
-- ***************
|
||
-- right, I think we rewrite the names in the context before running raw and we're good to go?
|
||
-- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was?
|
||
|
||
-- we could pass into build case and use it for (x /? y)
|
||
|
||
-- TODO, we may need to filter these against the type to rule out
|
||
-- impossible cases
|
||
getConstructors : Context -> FC -> Val -> M (List (QName × Int × Tm))
|
||
getConstructors ctx scfc (VRef fc nm _ _) = do
|
||
names <- lookupTCon nm
|
||
traverse lookupDCon names
|
||
where
|
||
lookupTCon : QName -> M (List QName)
|
||
lookupTCon str = do
|
||
top <- get
|
||
case lookup nm top of
|
||
(Just (MkEntry _ name type (TCon names))) => pure names
|
||
_ => error scfc "Not a type constructor \{show nm}"
|
||
lookupDCon : QName -> M (QName × Int × Tm)
|
||
lookupDCon nm = do
|
||
top <- get
|
||
case lookup nm top of
|
||
(Just (MkEntry _ name type (DCon k str))) => pure (name, k, type)
|
||
Just _ => error fc "Internal Error: \{show nm} is not a DCon"
|
||
Nothing => error fc "Internal Error: DCon \{show nm} not found"
|
||
getConstructors ctx scfc tm = do
|
||
tms <- vprint ctx tm
|
||
error scfc "Can't split - not VRef: \{tms}"
|
||
|
||
-- Extend environment with fresh variables from a pi-type
|
||
-- the pi-type here is the telescope of a constructor
|
||
-- return context, remaining type, and list of names
|
||
extendPi : Context -> Val -> SnocList Bind -> SnocList Val -> M (Context × Val × List Bind × SnocList Val)
|
||
extendPi ctx (VPi x str icit rig a b) nms sc = do
|
||
let nm = fresh str -- "pat"
|
||
let ctx' = extend ctx nm a
|
||
let v = VVar emptyFC (length' ctx.env) Lin
|
||
tyb <- b $$ v
|
||
extendPi ctx' tyb (nms :< MkBind nm icit a) (sc :< VVar x (length' ctx.env) Lin)
|
||
extendPi ctx ty nms sc = pure (ctx, ty, nms <>> Nil, sc)
|
||
|
||
-- turn vars into lets for forced values.
|
||
-- substitute inside values
|
||
-- FIXME we're not going under closures at the moment.
|
||
substVal : Int -> Val -> Val -> Val
|
||
substVal k v tm = go tm
|
||
where
|
||
go : Val -> Val
|
||
go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp))
|
||
go (VLet fc nm a b) = VLet fc nm (go a) b
|
||
go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b
|
||
go (VMeta fc ix sp) = VMeta fc ix (map go sp)
|
||
go (VRef fc nm y sp) = VRef fc nm y (map go sp)
|
||
go tm = tm
|
||
-- FIXME - do I need a Val closure like idris?
|
||
-- or env in unify...
|
||
-- or quote back
|
||
-- go (VLam fc nm sc) = VLam fc nm sc
|
||
-- go (VCase x sc xs) = ?rhs_2
|
||
-- go (VU x) = ?rhs_7
|
||
-- go (VLit x y) = ?rhs_8
|
||
|
||
|
||
-- need to turn k into a ground value
|
||
|
||
-- TODO rework this to do something better. We've got constraints, and
|
||
-- and may need to do proper unification if it's already defined to a value
|
||
-- below we're handling the case if it's defined to another var, but not
|
||
-- checking for loops.
|
||
updateContext : Context -> List (Int × Val) -> M Context
|
||
updateContext ctx Nil = pure ctx
|
||
updateContext ctx ((k, val) :: cs) =
|
||
let ix = cast $ lvl2ix (length' ctx.env) k in
|
||
case getAt ix ctx.env of
|
||
(Just (VVar _ k' Lin)) =>
|
||
if k' /= k
|
||
then updateContext ctx ((k',val) :: cs)
|
||
else
|
||
let ctx' = MkCtx ctx.lvl (map (substVal k val) ctx.env) ctx.types (replaceV ix Defined ctx.bds) ctx.ctxFC
|
||
in updateContext ctx' cs
|
||
(Just val') => do
|
||
-- This is fine for Z =?= Z but for other stuff, we probably have to match
|
||
info (getFC val) "need to unify \{show val} and \{show val'} or something"
|
||
updateContext ctx cs
|
||
Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext"
|
||
|
||
--
|
||
-- updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs
|
||
where
|
||
replace : Nat -> Val -> List Val -> List Val
|
||
replace k x Nil = Nil
|
||
replace Z x (y :: xs) = x :: xs
|
||
replace (S k) x (y :: xs) = y :: replace k x xs
|
||
|
||
replaceV : ∀ a. Nat -> a -> List a -> List a
|
||
replaceV k x Nil = Nil
|
||
replaceV Z x (y :: xs) = x :: xs
|
||
replaceV (S k) x (y :: xs) = y :: replaceV k x xs
|
||
|
||
-- ok, so this is a single constructor, CaseAlt
|
||
-- return Nothing if dcon doesn't unify with scrut
|
||
buildCase : Context -> Problem -> String -> Val -> (QName × Int × Tm) -> M (Maybe CaseAlt)
|
||
buildCase ctx prob scnm scty (dcName, arity, ty) = do
|
||
debug $ \ _ => "CASE \{scnm} match \{show dcName} ty \{rpprint (names ctx) ty}"
|
||
vty <- eval Nil CBN ty
|
||
(ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin
|
||
|
||
-- TODO I think we need to figure out what is dotted, maybe
|
||
-- the environment manipulation below is sufficient bookkeeping
|
||
-- or maybe it's a bad approach.
|
||
|
||
-- At some point, I'll take a break and review more papers and code,
|
||
-- now that I know some of the questions I'm trying to answer.
|
||
|
||
-- We get unification constraints from matching the data constructors
|
||
-- codomain with the scrutinee type
|
||
debug $ \ _ => "unify dcon cod with scrut\n \{show ty'}\n \{show scty}"
|
||
Just res <- catchError(Just <$> unify ctx'.env UPattern ty' scty)
|
||
(\err => do
|
||
debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}"
|
||
pure Nothing)
|
||
| _ => pure Nothing
|
||
|
||
-- if the value is already constrained to a different constructor, return Nothing
|
||
debug $ \ _ => "scrut \{scnm} constrained to \{show $ lookupDef ctx scnm}"
|
||
let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}"
|
||
|
||
case lookupDef ctx scnm of
|
||
Just val@(VRef fc nm y sp) =>
|
||
if nm /= dcName
|
||
then do
|
||
debug $ \ _ => "SKIP \{show dcName} because \{scnm} forced to \{show val}"
|
||
pure Nothing
|
||
else do
|
||
debug $ \ _ => "case \{show dcName} dotted \{show val}"
|
||
when (length vars /= snoclen sp) $ \ _ => error emptyFC "\{show $ length vars} vars /= \{show $ snoclen sp}"
|
||
|
||
-- TODO - I think we need to define the context vars to sp via updateContext
|
||
|
||
let lvl = length' ctx'.env - length' vars
|
||
let scons = constrainSpine lvl (sp <>> Nil) -- REVIEW is this the right order?
|
||
ctx' <- updateContext ctx' scons
|
||
|
||
debug $ \ _ => "(dcon \{show dcName} ty \{show ty'} scty \{show scty}"
|
||
debug $ \ _ => "(dcon \{show dcName}) (vars \{show vars}) clauses were"
|
||
for prob.clauses $ (\x => debug $ \ _ => " \{show x}")
|
||
clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses
|
||
debug $ \ _ => "and now:"
|
||
for clauses $ (\x => debug $ \ _ => " \{show x}")
|
||
when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show dcName} splitting \{scnm}"
|
||
tm <- buildTree ctx' (MkProb clauses prob.ty)
|
||
pure $ Just $ CaseCons dcName (map getName vars) tm
|
||
|
||
_ => do
|
||
(Right res) <- tryError (unify ctx'.env UPattern ty' scty)
|
||
| Left err => do
|
||
debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}"
|
||
pure Nothing
|
||
|
||
-- Constrain the scrutinee's variable to be dcon applied to args
|
||
let (Just x) = findIndex' ((_==_ scnm) ∘ fst) ctx'.types
|
||
| Nothing => error ctx.ctxFC "\{scnm} not is scope?"
|
||
let lvl = lvl2ix (length' ctx'.env) x
|
||
let scon = (lvl, VRef ctx.ctxFC dcName (DCon arity dcName) sc)
|
||
|
||
debug $ \ _ => "scty \{show scty}"
|
||
debug $ \ _ => "UNIFY results \{show res.constraints}"
|
||
debug $ \ _ => "before types: \{show ctx'.types}"
|
||
debug $ \ _ => "before env: \{show ctx'.env}"
|
||
debug $ \ _ => "SC CONSTRAINT: \{show scon}"
|
||
|
||
-- push the constraints into the environment by turning bind into define
|
||
-- Is this kosher? It might be a problem if we've already got metas over
|
||
-- this stuff, because it intends to ignore defines.
|
||
ctx' <- updateContext ctx' (scon :: res.constraints)
|
||
|
||
debug $ \ _ => "context types: \{show ctx'.types}"
|
||
debug $ \ _ => "context env: \{show ctx'.env}"
|
||
|
||
-- What if all of the pattern vars are defined to meta
|
||
|
||
debug $ \ _ => "(dcon \{show dcName} ty \{show ty'} scty \{show scty}"
|
||
debug $ \ _ => "(dcon \{show dcName}) (vars \{show vars}) clauses were"
|
||
for prob.clauses $ (\x => debug $ \ _ => " \{show x}")
|
||
clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses
|
||
debug $ \ _ => "and now:"
|
||
for clauses $ (\x => debug $ \ _ => " \{show x}")
|
||
when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show dcName} splitting \{scnm}"
|
||
tm <- buildTree ctx' (MkProb clauses prob.ty)
|
||
pure $ Just $ CaseCons dcName (map getName vars) tm
|
||
where
|
||
constrainSpine : Int -> List Val -> List (Int × Val)
|
||
constrainSpine lvl Nil = Nil
|
||
constrainSpine lvl (v :: vs) = (lvl, v) :: constrainSpine (1 + lvl) vs
|
||
|
||
getName : Bind -> String
|
||
getName (MkBind nm _ _) = nm
|
||
|
||
-- for each clause in prob, find nm on LHS of some constraint, and
|
||
-- "replace" with the constructor and vars.
|
||
--
|
||
-- This will be:
|
||
-- x /? y can probably just leave this
|
||
-- x /? D a b c split into three x /? a, y /? b, z /? c
|
||
-- x /? E a b drop this clause
|
||
-- We get a list of clauses back (a Problem) and then solve that
|
||
-- If they all fail, we have a coverage issue. (Assuming the constructor is valid)
|
||
|
||
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 ((MkBind nm Implicit x) :: xs) Nil = do
|
||
rest <- makeConstr xs Nil
|
||
pure $ (nm, PatWild emptyFC Implicit) :: rest
|
||
makeConstr ((MkBind nm Auto x) :: xs) Nil = do
|
||
rest <- makeConstr xs Nil
|
||
pure $ (nm, PatWild emptyFC Auto) :: rest
|
||
-- FIXME need a proper error, but requires wiring M three levels down
|
||
makeConstr ((MkBind nm Explicit x) :: xs) Nil = error ctx.ctxFC "not enough patterns"
|
||
makeConstr ((MkBind nm Explicit x) :: xs) (pat :: pats) =
|
||
if getIcit pat == Explicit
|
||
then do
|
||
rest <- makeConstr xs pats
|
||
pure $ (nm, pat) :: rest
|
||
else error ctx.ctxFC "mismatch between Explicit and \{show $ getIcit pat}"
|
||
makeConstr ((MkBind nm icit x) :: xs) (pat :: pats) =
|
||
if getIcit pat /= icit -- Implicit/Explicit Implicit/Auto, etc
|
||
then do
|
||
rest <- makeConstr xs (pat :: pats)
|
||
pure $ (nm, PatWild (getFC pat) icit) :: rest
|
||
else do
|
||
rest <- makeConstr xs pats
|
||
pure $ (nm, pat) :: rest
|
||
|
||
-- replace constraint with constraints on parameters, or nothing if non-matching clause
|
||
rewriteConstraint : QName -> List Bind -> List Constraint -> List Constraint -> M (Maybe (List Constraint))
|
||
rewriteConstraint sctynm vars Nil acc = pure $ Just acc
|
||
rewriteConstraint sctynm vars (c@(nm, y) :: xs) acc =
|
||
if nm == scnm
|
||
then case y of
|
||
PatVar _ _ s => pure $ Just $ c :: (xs ++ acc)
|
||
PatWild _ _ => pure $ Just $ c :: (xs ++ acc)
|
||
-- FIXME why don't we hit this (when user puts 'x' for Just 'x')
|
||
PatLit fc lit => error fc "Literal \{show lit} in constructor split"
|
||
PatCon fc icit nm ys as => if nm == dcName
|
||
then case as of
|
||
Nothing => do
|
||
rest <- makeConstr vars ys
|
||
pure $ Just $ rest ++ xs ++ acc
|
||
-- putting this in constraints causes it to be renamed scnm -> nm' when we check body.
|
||
Just nm' => do
|
||
rest <- makeConstr vars ys
|
||
pure $ Just $ (scnm, (PatVar fc icit nm')) :: rest ++ xs ++ acc
|
||
else do
|
||
-- TODO can we check this when we make the PatCon?
|
||
top <- get
|
||
case lookup nm top of
|
||
(Just (MkEntry _ name type (DCon k tcname))) =>
|
||
if (tcname /= sctynm)
|
||
then error fc "Constructor is \{show tcname} expected \{show sctynm}"
|
||
else pure Nothing
|
||
Just _ => error fc "Internal Error: \{show nm} is not a DCon"
|
||
Nothing => error fc "Internal Error: DCon \{show nm} not found"
|
||
else rewriteConstraint sctynm vars xs (c :: acc)
|
||
|
||
rewriteClause : QName -> List Bind -> Clause -> M (Maybe Clause)
|
||
rewriteClause sctynm vars (MkClause fc cons pats expr) = do
|
||
Just cons <- rewriteConstraint sctynm vars cons Nil | _ => pure Nothing
|
||
pure $ Just $ MkClause fc cons pats expr
|
||
|
||
|
||
splitArgs : Raw -> List (Raw × Icit) -> (Raw × List (Raw × Icit))
|
||
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)
|
||
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
|
||
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
|
||
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"
|
||
_ => case b of
|
||
Nil => pure $ PatVar fc icit nm
|
||
_ => error (getFC tm) "patvar applied to args"
|
||
((RImplicit fc), Nil) => pure $ PatWild fc icit
|
||
((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments"
|
||
((RLit fc lit), Nil) => pure $ PatLit fc lit
|
||
((RLit fc y), b) => error fc "lit cannot be applied to arguments"
|
||
(a,b) => error (getFC a) "expected pat var or constructor, got \{show a}"
|
||
|
||
|
||
|
||
makeClause : TopContext -> (Raw × Raw) -> M Clause
|
||
makeClause top (lhs, rhs) = do
|
||
let (nm, args) = splitArgs lhs Nil
|
||
pats <- traverse (mkPat top) args
|
||
pure $ MkClause (getFC lhs) Nil pats rhs
|
||
|
||
|
||
|
||
-- we'll want both check and infer, we're augmenting a context
|
||
-- so probably a continuation:
|
||
-- Context -> List Decl -> (Context -> M a) -> M a
|
||
checkWhere : Context -> List Decl -> Raw -> Val -> M Tm
|
||
checkWhere ctx decls body ty = do
|
||
-- we're going to be very proscriptive here
|
||
let (TypeSig sigFC (name :: Nil) rawtype :: decls) = decls
|
||
| x :: _ => error (getFC x) "expected type signature"
|
||
| _ => check ctx body ty
|
||
funTy <- check ctx rawtype (VU sigFC)
|
||
debug $ \ _ => "where clause \{name} : \{rpprint (names ctx) funTy}"
|
||
let (Def defFC name' clauses :: decls') = decls
|
||
| x :: _ => error (getFC x) "expected function definition"
|
||
| _ => error sigFC "expected function definition after this signature"
|
||
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
|
||
vty <- eval ctx.env CBN funTy
|
||
debug $ \ _ => "\{name} vty is \{show vty}"
|
||
let ctx' = extend ctx name vty
|
||
|
||
-- if I lift, I need to namespace it, add args, and add args when
|
||
-- calling locally
|
||
-- context could hold a Name -> Val (not Tm because levels) to help with that
|
||
-- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...)
|
||
-- But I'll attempt letrec first
|
||
tm <- buildTree (withPos ctx' defFC) (MkProb clauses' vty)
|
||
vtm <- eval ctx'.env CBN tm
|
||
-- Should we run the rest with the definition in place?
|
||
-- I'm wondering if switching from bind to define will mess with metas
|
||
-- let ctx' = define ctx name vtm vty
|
||
ty' <- checkWhere ctx' decls' body ty
|
||
pure $ LetRec sigFC name funTy tm ty'
|
||
|
||
|
||
checkDone : Context -> List (String × Pattern) -> Raw -> Val -> M Tm
|
||
checkDone ctx Nil body ty = do
|
||
debug $ \ _ => "DONE-> check body \{show body} at \{show ty}"
|
||
-- TODO better dump context function
|
||
debugM $ showCtx ctx
|
||
-- Hack to try to get Combinatory working
|
||
-- we're trying to subst in solutions here.
|
||
env' <- for ctx.env $ \ val => do
|
||
ty <- quote (length' ctx.env) val
|
||
-- This is not getting vars under lambdas
|
||
eval ctx.env CBV ty
|
||
types' <- for ctx.types $ \case
|
||
(nm,ty) => do
|
||
nty <- quote (length' env') ty
|
||
ty' <- eval env' CBV nty
|
||
pure (nm, ty')
|
||
let ctx = MkCtx ctx.lvl env' types' ctx.bds ctx.ctxFC
|
||
debug $ \ _ => "AFTER"
|
||
debugM $ showCtx ctx
|
||
-- I'm running an eval here to run case statements that are
|
||
-- unblocked by lets in the env. (Tree.newt:cmp)
|
||
-- The case eval code only works in the Tm -> Val case at the moment.
|
||
-- we don't have anything like `vapp` for case
|
||
ty <- quote (length' ctx.env) ty
|
||
ty <- eval ctx.env CBN ty
|
||
|
||
debug $ \ _ => "check at \{show ty}"
|
||
got <- check ctx body ty
|
||
debug $ \ _ => "DONE<- got \{rpprint (names ctx) got}"
|
||
pure got
|
||
checkDone ctx ((x, PatWild _ _) :: xs) body ty = checkDone ctx xs body ty
|
||
checkDone ctx ((nm, (PatVar _ _ nm')) :: xs) body ty =
|
||
let ctx = MkCtx ctx.lvl ctx.env (rename ctx.types) ctx.bds ctx.ctxFC in
|
||
checkDone ctx xs body ty
|
||
where
|
||
rename : List (String × Val) -> List (String × Val)
|
||
rename Nil = Nil
|
||
rename ((name, ty) :: xs) =
|
||
if name == nm
|
||
then (nm', ty) :: xs
|
||
else (name, ty) :: rename xs
|
||
|
||
checkDone ctx ((x, pat) :: xs) body ty = error (getFC pat) "stray constraint \{x} /? \{show pat}"
|
||
|
||
-- need to run constructors, then run default
|
||
|
||
-- wild/var can come before 'x' so we need a list first
|
||
getLits : String -> List Clause -> List Literal
|
||
getLits nm Nil = Nil
|
||
getLits nm ((MkClause fc cons pats expr) :: cs) = case find ((_==_ nm) ∘ fst) cons of
|
||
Just (_, (PatLit _ lit)) => lit :: getLits nm cs
|
||
_ => getLits nm cs
|
||
|
||
|
||
-- then build a lit case for each of those
|
||
|
||
buildLitCase : Context -> Problem -> FC -> String -> Val -> Literal -> M CaseAlt
|
||
buildLitCase ctx prob fc scnm scty lit = do
|
||
|
||
-- Constrain the scrutinee's variable to be lit value
|
||
let (Just ix) = findIndex' ((_==_ scnm) ∘ fst) ctx.types
|
||
| Nothing => error ctx.ctxFC "\{scnm} not is scope?"
|
||
let lvl = lvl2ix (length' ctx.env) ix
|
||
let scon = (lvl, VLit fc lit)
|
||
ctx' <- updateContext ctx (scon :: Nil)
|
||
let clauses = mapMaybe rewriteClause prob.clauses
|
||
|
||
when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show lit} splitting \{scnm}"
|
||
tm <- buildTree ctx' (MkProb clauses prob.ty)
|
||
pure $ CaseLit lit tm
|
||
|
||
where
|
||
-- FIXME - thread in M for errors
|
||
-- replace constraint with constraints on parameters, or nothing if non-matching clause
|
||
rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint)
|
||
rewriteConstraint Nil acc = Just acc
|
||
rewriteConstraint (c@(nm, y) :: xs) acc =
|
||
if nm == scnm
|
||
then case y of
|
||
PatVar _ _ s => Just $ c :: (xs ++ acc)
|
||
PatWild _ _ => Just $ c :: (xs ++ acc)
|
||
PatLit fc lit' => if lit' == lit then Just $ (xs ++ acc) else Nothing
|
||
PatCon _ _ str ys as => Nothing -- error matching lit against constructor
|
||
else rewriteConstraint xs (c :: acc)
|
||
|
||
rewriteClause : Clause -> Maybe Clause
|
||
rewriteClause (MkClause fc cons pats expr) = do
|
||
cons <- rewriteConstraint cons Nil
|
||
pure $ MkClause fc cons pats expr
|
||
|
||
|
||
|
||
buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt)
|
||
buildLitCases ctx prob fc scnm scty = do
|
||
let lits = nub $ getLits scnm prob.clauses
|
||
alts <- traverse (buildLitCase ctx prob fc scnm scty) lits
|
||
-- TODO build default case
|
||
-- run getLits
|
||
-- buildLitCase for each
|
||
|
||
let defclauses = filter isDefault prob.clauses
|
||
when (length' defclauses == 0) $ \ _ => error fc "no default for literal slot on \{show scnm}"
|
||
tm <- buildTree ctx (MkProb defclauses prob.ty)
|
||
|
||
pure $ alts ++ ( CaseDefault tm :: Nil)
|
||
where
|
||
isDefault : Clause -> Bool
|
||
isDefault cl = case find ((_==_ scnm) ∘ fst) cl.cons of
|
||
Just (_, (PatVar _ _ _)) => True
|
||
Just (_, (PatWild _ _)) => True
|
||
Nothing => True
|
||
_ => False
|
||
|
||
-- TODO - figure out if these need to be in Prelude or have a special namespace
|
||
-- If we lookupRaw "String", we could get different answers in different contexts.
|
||
-- maybe Hardwire this one
|
||
stringType intType charType : QName
|
||
stringType = QN ("Prim" :: Nil) "String"
|
||
intType = QN ("Prim" :: Nil) "Int"
|
||
charType = QN ("Prim" :: Nil) "Char"
|
||
|
||
litTyName : Literal -> QName
|
||
litTyName (LString str) = stringType
|
||
litTyName (LInt i) = intType
|
||
litTyName (LChar c) = charType
|
||
|
||
renameContext : String -> String -> Context -> Context
|
||
renameContext from to ctx = MkCtx ctx.lvl ctx.env (go ctx.types) ctx.bds ctx.ctxFC
|
||
where
|
||
go : List (String × Val) -> List (String × Val)
|
||
go Nil = Nil
|
||
go ((a,b) :: types) = if a == from then (to,b) :: types else (a,b) :: go types
|
||
|
||
-- This process is similar to extendPi, but we need to stop
|
||
-- if one clause is short on patterns.
|
||
buildTree ctx (MkProb Nil ty) = error emptyFC "no clauses"
|
||
buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit rig a b)) = do
|
||
let l = length' ctx.env
|
||
let nm = fresh str -- "pat"
|
||
let ctx' = extend ctx nm a
|
||
-- type of the rest
|
||
clauses <- traverse (introClause nm icit) prob.clauses
|
||
-- REVIEW fc from a pat?
|
||
vb <- b $$ VVar fc l Lin
|
||
Lam fc nm icit rig <$> buildTree ctx' (MkProb clauses vb)
|
||
buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) =
|
||
error fc "Extra pattern variables \{show pats}"
|
||
-- need to find some name we can split in (x :: xs)
|
||
-- so LHS of constraint is name (or VVar - if we do Val)
|
||
-- then run the split
|
||
-- some of this is copied into check
|
||
buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
|
||
debug $ \ _ => "buildTree \{show constraints} \{show expr}"
|
||
let (Just (scnm, pat)) = findSplit constraints
|
||
| _ => do
|
||
debug $ \ _ => "checkDone \{show constraints}"
|
||
checkDone ctx constraints expr ty
|
||
|
||
debug $ \ _ => "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}"
|
||
let (Just (sctm, scty)) = lookupName ctx scnm
|
||
| _ => error fc "Internal Error: can't find \{scnm} in environment"
|
||
|
||
-- REVIEW We probably need to know this is a VRef before we decide to split on this slot..
|
||
scty' <- unlet ctx.env scty >>= forceType ctx.env
|
||
-- TODO attempting to pick up Autos that could have been solved immediately
|
||
-- If we try on creation, we're looping at the moment, because of the possibility
|
||
-- of Ord a -> Ord b -> Ord (a \x b). Need to cut earlier when solving or switch to
|
||
-- Idris method...
|
||
scty' <- case scty' of
|
||
(VMeta fc1 ix sp) => do
|
||
meta <- lookupMeta ix
|
||
case meta of
|
||
(Solved _ k t) => forceType ctx.env scty'
|
||
(Unsolved _ k xs _ _ _) => do
|
||
top <- get
|
||
mc <- readIORef top.metaCtx
|
||
ignore $ solveAutos 0
|
||
forceType ctx.env scty'
|
||
|
||
_ => pure scty'
|
||
|
||
case pat of
|
||
PatCon fc _ _ _ as => do
|
||
-- expand vars that may be solved, eval top level functions
|
||
debug $ \ _ => "EXP \{show scty} -> \{show scty'}"
|
||
-- this is per the paper, but it would be nice to coalesce
|
||
-- default cases
|
||
cons <- getConstructors ctx (getFC pat) scty'
|
||
debug $ \ _ => "CONS \{show $ map fst cons}"
|
||
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'}"
|
||
pure $ Case fc sctm (mapMaybe id alts)
|
||
PatLit fc v => do
|
||
let tyname = litTyName v
|
||
case scty' of
|
||
(VRef fc1 nm x sp) => when (nm /= tyname) $ \ _ => error fc "expected \{show scty} and got \{show tyname}"
|
||
_ => error fc "expected \{show scty} and got \{show tyname}"
|
||
-- need to run through all of the PatLits in this slot and then find a fallback
|
||
-- walk the list of patterns, stop if we hit a PatVar / PatWild, fail if we don't
|
||
alts <- buildLitCases ctx prob fc scnm scty
|
||
pure $ Case fc sctm alts
|
||
pat => error (getFC pat) "Internal error - tried to split on \{show pat}"
|
||
|
||
showDef : Context -> List String -> Int -> Val -> M String
|
||
showDef ctx names n v@(VVar _ n' Lin) = if n == n'
|
||
then pure ""
|
||
else do
|
||
-- REVIEW - was using names, is it ok to pull from the context?
|
||
vv <- vprint ctx v
|
||
pure "= \{vv}"
|
||
showDef ctx names n v = do
|
||
vv <- vprint ctx v
|
||
pure "= \{vv}"
|
||
-- pure "= \{rpprint names !(quote ctx.lvl v)}"
|
||
|
||
-- desugar do
|
||
undo : FC -> List DoStmt -> M Raw
|
||
undo prev Nil = error prev "do block must end in expression"
|
||
undo prev ((DoExpr fc tm) :: Nil) = pure tm
|
||
-- TODO decide if we want to use >> or just >>=
|
||
undo prev ((DoExpr fc tm) :: xs) = do
|
||
xs' <- undo fc xs
|
||
pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit
|
||
undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs
|
||
undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
|
||
top <- get
|
||
case lookupRaw nm top of
|
||
Just _ => do
|
||
let nm = "$sc"
|
||
xs' <- undo fc xs
|
||
rest <- pure $ RCase fc (RVar fc nm) (MkAlt left xs' :: Nil)
|
||
pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
|
||
(RLam fc (BI fc nm Explicit Many) rest) Explicit
|
||
Nothing => do
|
||
xs' <- undo fc xs
|
||
pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
|
||
(RLam fc (BI fc' nm Explicit Many) xs') Explicit
|
||
undo prev ((DoArrow fc left right alts) :: xs) = do
|
||
let nm = "$sc"
|
||
xs' <- undo fc xs
|
||
rest <- pure $ RCase fc (RVar fc nm) (MkAlt left xs' :: alts)
|
||
pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
|
||
(RLam fc (BI fc nm Explicit Many) rest) Explicit
|
||
|
||
check ctx tm ty = do
|
||
ty' <- forceType ctx.env ty
|
||
case (tm, ty') of
|
||
(RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty
|
||
(RIf fc a b c, ty) =>
|
||
let tm' = RCase fc a ( MkAlt (RVar (getFC b) "True") b :: MkAlt (RVar (getFC c) "False") c :: Nil) in
|
||
check ctx tm' ty
|
||
(RDo fc stmts, ty) => do
|
||
stmts' <- undo fc stmts
|
||
check ctx stmts' ty
|
||
(RCase fc rsc alts, ty) => do
|
||
(sc, scty) <- infer ctx rsc
|
||
scty <- forceMeta scty
|
||
debug $ \ _ => "SCTM \{rpprint (names ctx) sc}"
|
||
debug $ \ _ => "SCTY \{show scty}"
|
||
|
||
let scnm = fresh "sc"
|
||
top <- get
|
||
clauses <- for alts $ \case
|
||
(MkAlt pat rawRHS) => do
|
||
pat' <- mkPat top (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.
|
||
let ctx' = extend ctx scnm scty
|
||
tree <- buildTree ctx' $ MkProb clauses ty
|
||
pure $ Let fc scnm sc tree
|
||
|
||
-- rendered in ProcessDecl
|
||
(RHole fc, ty) => freshMeta ctx fc ty User
|
||
|
||
(t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' rig a b)) => do
|
||
debug $ \ _ => "icits \{nm} \{show icit} \{nm'} \{show icit'}"
|
||
if icit == icit' then do
|
||
let var = VVar fc (length' ctx.env) Lin
|
||
let ctx' = extend ctx nm a
|
||
bapp <- b $$ var
|
||
tm' <- check ctx' tm bapp
|
||
pure $ Lam fc nm icit rig tm'
|
||
else if icit' /= Explicit then do
|
||
let var = VVar fc (length' ctx.env) Lin
|
||
ty' <- b $$ var
|
||
-- use nm' here if we want them automatically in scope
|
||
sc <- check (extend ctx nm' a) t ty'
|
||
pure $ Lam fc nm' icit rig sc
|
||
else
|
||
error fc "Icity issue checking \{show t} at \{show ty}"
|
||
(t@(RLam _ (BI fc nm icit quant) tm), ty) => do
|
||
pty <- prvalCtx ty
|
||
error fc "Expected pi type, got \{pty}"
|
||
|
||
|
||
(RLet fc nm ty v sc, rty) => do
|
||
ty' <- check ctx ty (VU emptyFC)
|
||
vty <- eval ctx.env CBN ty'
|
||
v' <- check ctx v vty
|
||
vv <- eval ctx.env CBN v'
|
||
let ctx' = define ctx nm vv vty
|
||
sc' <- check ctx' sc rty
|
||
pure $ Let fc nm v' sc'
|
||
|
||
(RImplicit fc, ty) => freshMeta ctx fc ty Normal
|
||
|
||
(tm, ty@(VPi fc nm' Implicit rig a b)) => do
|
||
let names = map fst ctx.types
|
||
debug $ \ _ => "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} "
|
||
let var = VVar fc (length' ctx.env) Lin
|
||
ty' <- b $$ var
|
||
debugM $ do
|
||
pty' <- prvalCtx {{(extend ctx nm' a)}} ty'
|
||
pure "XXX ty' is \{pty'}"
|
||
sc <- check (extend ctx nm' a) tm ty'
|
||
pure $ Lam (getFC tm) nm' Implicit rig sc
|
||
|
||
(tm, ty@(VPi fc nm' Auto rig a b)) => do
|
||
let names = map fst ctx.types
|
||
debug $ \ _ => "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} "
|
||
let var = VVar fc (length' ctx.env) Lin
|
||
ty' <- b $$ var
|
||
debugM $ do
|
||
pty' <- prvalCtx {{(extend ctx nm' a)}} ty'
|
||
pure "XXX ty' is \{pty'}"
|
||
sc <- check (extend ctx nm' a) tm ty'
|
||
pure $ Lam (getFC tm) nm' Auto rig sc
|
||
|
||
(tm,ty) => do
|
||
(tm', ty') <- infer ctx tm
|
||
(tm', ty') <- insert ctx tm' ty'
|
||
|
||
let names = map fst ctx.types
|
||
debug $ \ _ => "INFER \{show tm} to (\{rpprint names tm'} : \{show ty'}) expect \{show ty}"
|
||
unifyCatch (getFC tm) ctx ty' ty
|
||
pure tm'
|
||
|
||
infer ctx (RVar fc nm) = go 0 ctx.types
|
||
where
|
||
go : Int -> List (String × Val) -> M (Tm × Val)
|
||
go i Nil = do
|
||
top <- get
|
||
case lookupRaw nm top of
|
||
Just (MkEntry _ name ty def) => do
|
||
debug $ \ _ => "lookup \{show name} as \{show def}"
|
||
vty <- eval Nil CBN ty
|
||
pure (Ref fc name def, vty)
|
||
Nothing => error fc "\{show nm} not in scope"
|
||
go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty)
|
||
else go (i + 1) xs
|
||
-- FIXME tightens up output but hardcodes a name
|
||
-- infer ctx (RApp fc (RVar _ "_$_") u icit) = infer ctx u
|
||
infer ctx (RApp fc t u icit) = do
|
||
-- If the app is explicit, add any necessary metas
|
||
(icit, t, tty) <- case the Icit icit of
|
||
Explicit => do
|
||
(t, tty) <- infer ctx t
|
||
(t, tty) <- insert ctx t tty
|
||
pure (Explicit, t, tty)
|
||
Implicit => do
|
||
(t, tty) <- infer ctx t
|
||
pure (Implicit, t, tty)
|
||
Auto => do
|
||
(t, tty) <- infer ctx t
|
||
pure (Auto, t, tty)
|
||
|
||
(a,b) <- do
|
||
tty' <- forceMeta tty
|
||
case tty' of
|
||
(VPi fc' str icit' rig a b) => if icit' == icit then pure (a,b)
|
||
else error fc "IcitMismatch \{show icit} \{show icit'}"
|
||
|
||
-- If it's not a VPi, try to unify it with a VPi
|
||
-- TODO test case to cover this.
|
||
tty => do
|
||
debug $ \ _ => "unify PI for \{show tty}"
|
||
a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN
|
||
b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal
|
||
-- FIXME - I had to guess Many here. What are the side effects?
|
||
unifyCatch fc ctx tty (VPi fc ":ins" icit Many a b)
|
||
pure (a,b)
|
||
|
||
u <- check ctx u a
|
||
u' <- eval ctx.env CBN u
|
||
bappu <- b $$ u'
|
||
pure (App fc t u, bappu)
|
||
|
||
infer ctx (RU fc) = pure (UU fc, VU fc) -- YOLO
|
||
infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do
|
||
ty' <- check ctx ty (VU fc)
|
||
vty' <- eval ctx.env CBN ty'
|
||
ty2' <- check (extend ctx nm vty') ty2 (VU fc)
|
||
pure (Pi fc nm icit quant ty' ty2', (VU fc))
|
||
infer ctx (RLet fc nm ty v sc) = do
|
||
ty' <- check ctx ty (VU emptyFC)
|
||
vty <- eval ctx.env CBN ty'
|
||
v' <- check ctx v vty
|
||
vv <- eval ctx.env CBN v'
|
||
let ctx' = define ctx nm vv vty
|
||
(sc',scty) <- infer ctx' sc
|
||
pure $ (Let fc nm v' sc', scty)
|
||
|
||
infer ctx (RAnn fc tm rty) = do
|
||
ty <- check ctx rty (VU fc)
|
||
vty <- eval ctx.env CBN ty
|
||
tm <- check ctx tm vty
|
||
pure (tm, vty)
|
||
|
||
infer ctx (RLam _ (BI fc nm icit quant) tm) = do
|
||
a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN
|
||
let ctx' = extend ctx nm a
|
||
(tm', b) <- infer ctx' tm
|
||
debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}"
|
||
tyb <- quote (1 + ctx.lvl) b
|
||
pure $ (Lam fc nm icit quant tm', VPi fc nm icit quant a (MkClosure ctx.env tyb))
|
||
|
||
infer ctx (RImplicit fc) = do
|
||
ty <- freshMeta ctx fc (VU emptyFC) Normal
|
||
vty <- eval ctx.env CBN ty
|
||
tm <- freshMeta ctx fc vty Normal
|
||
pure (tm, vty)
|
||
|
||
infer ctx (RLit fc (LString str)) = do
|
||
ty <- primType fc stringType
|
||
pure (Lit fc (LString str), ty)
|
||
infer ctx (RLit fc (LInt i)) = do
|
||
ty <- primType fc intType
|
||
pure (Lit fc (LInt i), ty)
|
||
infer ctx (RLit fc (LChar c)) = do
|
||
ty <- primType fc charType
|
||
pure (Lit fc (LChar c), ty)
|
||
infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns"
|
||
infer ctx tm = error (getFC tm) "Implement infer \{show tm}"
|