move auto solver to elab
This commit is contained in:
145
src/Lib/Elab.idr
145
src/Lib/Elab.idr
@@ -11,6 +11,9 @@ import Lib.Eval
|
||||
import Lib.TopContext
|
||||
import Lib.Syntax
|
||||
|
||||
|
||||
|
||||
|
||||
||| collectDecl collects multiple Def for one function into one
|
||||
export
|
||||
collectDecl : List Decl -> List Decl
|
||||
@@ -92,6 +95,124 @@ Monoid UnifyResult where
|
||||
|
||||
data UnifyMode = Normal | Pattern
|
||||
|
||||
|
||||
export
|
||||
check : Context -> Raw -> Val -> M Tm
|
||||
|
||||
export
|
||||
unifyCatch : FC -> Context -> Val -> Val -> M ()
|
||||
|
||||
-- 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
|
||||
export
|
||||
findMatches : Context -> Val -> List TopEntry -> M (List (Tm, MetaContext))
|
||||
findMatches ctx ty [] = pure []
|
||||
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 \{name} : \{pprint [] 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 \{pprint [] tm} for \{show ty}"
|
||||
mc' <- readIORef top.metaCtx
|
||||
writeIORef top.metaCtx mc
|
||||
((tm, mc') ::) <$> findMatches ctx ty xs)
|
||||
(\ err => do
|
||||
debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
|
||||
writeIORef top.metaCtx mc
|
||||
findMatches ctx ty xs)
|
||||
|
||||
export
|
||||
contextMatches : Context -> Val -> M (List (Tm, MetaContext))
|
||||
contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
|
||||
where
|
||||
go : List (Val, String, Val) -> M (List (Tm, MetaContext))
|
||||
go [] = pure []
|
||||
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} : \{pprint (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, mc') ::) <$> go xs)
|
||||
(\ err => do
|
||||
debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}"
|
||||
writeIORef top.metaCtx mc
|
||||
go xs)
|
||||
|
||||
export
|
||||
getArity : Tm -> Nat
|
||||
getArity (Pi x str icit rig t u) = S (getArity u)
|
||||
-- Ref or App (of type constructor) are valid
|
||||
getArity _ = Z
|
||||
|
||||
-- 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 : Nat -> Vect k BD -> SnocList Val
|
||||
makeSpine k [] = [<]
|
||||
makeSpine (S k) (Defined :: xs) = makeSpine k xs
|
||||
makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<]
|
||||
makeSpine 0 xs = ?fixme
|
||||
|
||||
export
|
||||
solve : Env -> (k : Nat) -> SnocList Val -> Val -> M ()
|
||||
|
||||
export
|
||||
solveAutos : Nat -> List MetaEntry -> M ()
|
||||
solveAutos mstart [] = pure ()
|
||||
solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
|
||||
debug "AUTO 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
|
||||
[(tm, mc)] <- case !(contextMatches ctx ty) of
|
||||
[] => findMatches ctx ty $ toList top.defs
|
||||
xs => pure xs
|
||||
| res => do
|
||||
debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
|
||||
solveAutos mstart es
|
||||
writeIORef top.metaCtx mc
|
||||
val <- eval ctx.env CBN tm
|
||||
debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
|
||||
let sp = makeSpine ctx.lvl ctx.bds
|
||||
solve ctx.env k sp val
|
||||
mc <- readIORef top.metaCtx
|
||||
let mlen = length mc.metas `minus` mstart
|
||||
solveAutos mstart (take mlen mc.metas)
|
||||
solveAutos mstart (_ :: es) = solveAutos mstart es
|
||||
|
||||
|
||||
-- We need to switch to SortedMap here
|
||||
export
|
||||
updateMeta : Nat -> (MetaEntry -> M MetaEntry) -> M ()
|
||||
@@ -191,8 +312,6 @@ unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult
|
||||
(.boundNames) : Context -> List String
|
||||
ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ toList $ zip ctx.bds (map fst ctx.types)
|
||||
|
||||
export
|
||||
solve : Env -> (k : Nat) -> SnocList Val -> Val -> M ()
|
||||
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]"
|
||||
@@ -361,8 +480,7 @@ unify env mode t u = do
|
||||
unifyPattern t (VVar fc k [<]) = pure $ MkResult [(k, t)]
|
||||
unifyPattern t u = unifyMeta t u
|
||||
|
||||
export
|
||||
unifyCatch : FC -> Context -> Val -> Val -> M ()
|
||||
|
||||
unifyCatch fc ctx ty' ty = do
|
||||
res <- catchError (unify ctx.env Normal ty' ty) $ \err => do
|
||||
let names = toList $ map fst ctx.types
|
||||
@@ -385,6 +503,23 @@ unifyCatch fc ctx ty' ty = do
|
||||
throwError (E fc msg)
|
||||
-- error fc "Unification yields constraints \{show cs.constraints}"
|
||||
|
||||
export
|
||||
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 []
|
||||
writeIORef top.metaCtx $ { next $= S, metas $= (newmeta ::) } mc
|
||||
pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
|
||||
where
|
||||
-- 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
|
||||
|
||||
insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
|
||||
insert ctx tm ty = do
|
||||
case !(forceMeta ty) of
|
||||
@@ -410,8 +545,6 @@ primType fc nm = case lookup nm !(get) of
|
||||
export
|
||||
infer : Context -> Raw -> M (Tm, Val)
|
||||
|
||||
export
|
||||
check : Context -> Raw -> Val -> M Tm
|
||||
|
||||
data Bind = MkBind String Icit Val
|
||||
|
||||
|
||||
@@ -15,111 +15,6 @@ import Lib.Types
|
||||
import Lib.Util
|
||||
import Lib.Erasure
|
||||
|
||||
-- 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
|
||||
-- TODO consider ctx
|
||||
findMatches : Context -> Val -> List TopEntry -> M (List (Tm, MetaContext))
|
||||
findMatches ctx ty [] = pure []
|
||||
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 \{name} : \{pprint [] 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 \{pprint [] tm} for \{show ty}"
|
||||
mc' <- readIORef top.metaCtx
|
||||
writeIORef top.metaCtx mc
|
||||
((tm, mc') ::) <$> findMatches ctx ty xs)
|
||||
(\ err => do
|
||||
debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
|
||||
writeIORef top.metaCtx mc
|
||||
findMatches ctx ty xs)
|
||||
|
||||
contextMatches : Context -> Val -> M (List (Tm, MetaContext))
|
||||
contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
|
||||
where
|
||||
go : List (Val, String, Val) -> M (List (Tm, MetaContext))
|
||||
go [] = pure []
|
||||
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} : \{pprint (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, mc') ::) <$> go xs)
|
||||
(\ err => do
|
||||
debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}"
|
||||
writeIORef top.metaCtx mc
|
||||
go xs)
|
||||
|
||||
-- FIXME - decide if we want to count Zero here
|
||||
getArity : Tm -> Nat
|
||||
getArity (Pi x str icit rig t u) = S (getArity u)
|
||||
-- Ref or App (of type constructor) are valid
|
||||
getArity _ = Z
|
||||
|
||||
-- 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 : Nat -> Vect k BD -> SnocList Val
|
||||
makeSpine k [] = [<]
|
||||
makeSpine (S k) (Defined :: xs) = makeSpine k xs
|
||||
makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<]
|
||||
makeSpine 0 xs = ?fixme
|
||||
|
||||
solveAutos : Nat -> List MetaEntry -> M ()
|
||||
solveAutos mstart [] = pure ()
|
||||
solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
|
||||
debug "AUTO 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
|
||||
[(tm, mc)] <- case !(contextMatches ctx ty) of
|
||||
[] => findMatches ctx ty $ toList top.defs
|
||||
xs => pure xs
|
||||
| res => do
|
||||
debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
|
||||
solveAutos mstart es
|
||||
writeIORef top.metaCtx mc
|
||||
val <- eval ctx.env CBN tm
|
||||
debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
|
||||
let sp = makeSpine ctx.lvl ctx.bds
|
||||
solve ctx.env k sp val
|
||||
mc <- readIORef top.metaCtx
|
||||
let mlen = length mc.metas `minus` mstart
|
||||
solveAutos mstart (take mlen mc.metas)
|
||||
solveAutos mstart (_ :: es) = solveAutos mstart es
|
||||
|
||||
dumpEnv : Context -> M String
|
||||
dumpEnv ctx =
|
||||
unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) []
|
||||
|
||||
@@ -572,21 +572,6 @@ export
|
||||
error' : String -> M a
|
||||
error' msg = throwError $ E emptyFC msg
|
||||
|
||||
export
|
||||
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})"
|
||||
writeIORef top.metaCtx $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
|
||||
pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
|
||||
where
|
||||
-- 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
|
||||
|
||||
export
|
||||
lookupMeta : Nat -> M MetaEntry
|
||||
|
||||
Reference in New Issue
Block a user