edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-30 12:14:17 +03:00
Code Issues Projects Releases Wiki Activity

Add a 'staging area' to contexts

Browse Source 
This is for updates we make while branching in an elaborator - we don't
want to update the context immediately, because if the branch fails,
we'll need to revert, so for safety we'll note the updates we're going
to make and only complete the update when we're back at the top level.
This commit is contained in:
Edwin Brady 2019-05-03 02:43:47 +01:00
parent 29a41ed975
commit bfe78baf07
16 changed files with 462 additions and 209 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

64
src/Core/AutoSearch.idr
View File

@ -16,6 +16,7 @@ SearchEnv vars = List (NF vars, Closure vars)
searchType : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defining : Name) -> (topTy : Term vars) ->
Env Term vars -> SearchEnv vars ->
(target : NF vars) -> Core (NF vars)
@ -24,6 +25,7 @@ export
search : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defining : Name) -> (topTy : Term vars) -> Env Term vars ->
Core (Term vars)
@ -49,7 +51,7 @@ mkArgs fc rigc env (NBind nfc x (Pi c p ty) sc)
(idx, arg) <- newMeta fc argRig env nm argTy
-- setInvertible fc argName
(rest, restTy) <- mkArgs fc rigc env
!(sc (toClosure defaultOpts env arg))
!(sc defs (toClosure defaultOpts env arg))
pure (MkArgInfo idx argRig (appInf Nothing p) arg ty :: rest, restTy)
mkArgs fc rigc env ty = pure ([], ty)
@ -62,11 +64,14 @@ closureApply _ _ _ = throw (InternalError "Wrong argument form in AutoSearch")
searchIfHole : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC ->
(defaults : Bool) -> (depth : Nat) ->
(defining : Name) -> (topTy : Term vars) -> Env Term vars ->
SearchEnv vars ->
(arg : ArgInfo vars) ->
Core ()
searchIfHole fc def top env locs arg
searchIfHole fc defaults Z def top env locs arg
= throw (CantSolveGoal fc env top) -- possibly should say depth limit hit?
searchIfHole fc defaults (S depth) def top env locs arg
= do let hole = holeID arg
let rig = argRig arg
@ -75,21 +80,23 @@ searchIfHole fc def top env locs arg
| Nothing => throw (CantSolveGoal fc env top)
let Hole inv = definition gdef
| _ => pure () -- already solved
argdef <- searchType fc rig def top env locs (argType arg)
argdef <- searchType fc rig defaults depth def top env locs (argType arg)
vs <- unify InTerm fc env !(nf defs env (metaApp arg)) argdef
let [] = constraints vs
| _ => throw (CantSolveGoal fc env top)
pure ()
searchLocal : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defining : Name) -> (topTy : Term vars) ->
Env Term vars -> SearchEnv vars -> SearchEnv vars ->
(target : NF vars) -> Core (NF vars)
searchLocal fc rigc def top env locs [] target
searchLocal fc rigc defaults depth def top env locs [] target
= throw (CantSolveGoal fc env top)
searchLocal fc rigc def top env locs ((ty, c) :: rest) target
searchLocal fc rigc defaults depth def top env locs ((ty, c) :: rest) target
= tryUnify
(do (args, appTy) <- mkArgs fc rigc env ty
-- TODO: Can only use the local if it's not an unsolved hole
@ -97,21 +104,50 @@ searchLocal fc rigc def top env locs ((ty, c) :: rest) target
let [] = constraints ures
| _ => throw (CantSolveGoal fc env top)
candidate <- closureApply fc c args
traverse (searchIfHole fc def top env locs) args
traverse (searchIfHole fc defaults depth def top env locs) args
defs <- get Ctxt
nf defs env candidate)
(searchLocal fc rigc def top env locs rest target)
(searchLocal fc rigc defaults depth def top env locs rest target)
searchType fc rigc def top env locs (NBind nfc x (Pi c p ty) sc)
= pure (NBind nfc x (Lam c p ty)
(\arg => searchType fc rigc def top env ((ty, arg) :: locs) !(sc arg)))
searchType fc rigc def top env locs target
= searchLocal fc rigc def top env locs locs target
searchNames : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defining : Name) -> (topTy : Term vars) ->
Env Term vars -> List Name ->
(target : NF vars) -> Core (NF vars)
-- Declared at the top
search fc rigc def top env
searchType fc rigc defaults depth def top env locs (NBind nfc x (Pi c p ty) sc)
= pure (NBind nfc x (Lam c p ty)
(\defs, arg => searchType fc rigc defaults depth def top env
((ty, arg) :: locs) !(sc defs arg)))
searchType {vars} fc rigc defaults depth def top env locs target@(NTCon tfc tyn t a args)
= if a == length args
then do sd <- getSearchData fc defaults tyn
-- TODO: Check determining arguments are okay for 'args'
tryGroups (hintGroups sd)
else throw (CantSolveGoal fc env top)
where
ambig : Error -> Bool
ambig (AmbiguousSearch _ _ _) = True
ambig _ = False
tryGroups : List (List Name) -> Core (NF vars)
tryGroups [] = throw (CantSolveGoal fc env top)
tryGroups (g :: gs)
= handleUnify
(searchNames fc rigc defaults depth def top env g target)
(\err => if ambig err || isNil gs
then throw err
else tryGroups gs)
searchType fc rigc defaults depth def top env locs target
= searchLocal fc rigc defaults depth def top env locs locs target
-- Declared at the top
search fc rigc defaults depth def top env
= do defs <- get Ctxt
tm <- searchType fc rigc def top env []
tm <- searchType fc rigc defaults depth def top env []
!(nf defs env top)
empty <- clearDefs defs
quote empty env tm

13
src/Core/Binary.idr
View File

@ -9,6 +9,7 @@ import Core.TTC
import Core.UnifyState
import Data.IntMap
import Data.NameMap
-- Reading and writing 'Defs' from/to a binary file
-- In order to be saved, a name must have been flagged using 'toSave'.
@ -48,6 +49,8 @@ record TTCFile extra where
guesses : List (Int, (FC, Name))
constraints : List (Int, Constraint)
context : List GlobalDef
autoHints : List (Name, Bool)
typeHints : List (Name, Name, Bool)
imported : List (List String, Bool, List String)
nextVar : Int
currentNS : List String
@ -101,6 +104,8 @@ writeTTCFile b file
toBuf b (guesses file)
toBuf b (constraints file)
toBuf b (context file)
toBuf b (autoHints file)
toBuf b (typeHints file)
toBuf b (imported file)
toBuf b (nextVar file)
toBuf b (currentNS file)
@ -129,13 +134,16 @@ readTTCFile modns as r b
constraints <- the (Core (List (Int, Constraint))) $ fromBuf r b
coreLift $ putStrLn $ "Read " ++ show (length constraints) ++ " constraints"
defs <- fromBuf r b
autohs <- fromBuf r b
typehs <- fromBuf r b
-- coreLift $ putStrLn $ "Read " ++ show (length (map fullname defs)) ++ " defs"
imp <- fromBuf r b
nextv <- fromBuf r b
cns <- fromBuf r b
ex <- fromBuf r b
pure (MkTTCFile ver ifaceHash importHashes r
holes guesses constraints defs imp nextv cns ex)
holes guesses constraints defs
autohs typehs imp nextv cns ex)
-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : List Name -> List GlobalDef -> Defs -> Core (List GlobalDef)
@ -167,6 +175,8 @@ writeToTTC extradata fname
(toList (guesses ust))
(toList (constraints ust))
gdefs
(toList (autoHints defs))
(typeHints defs)
(imported defs)
(nextName ust)
(currentNS defs)
@ -216,6 +226,7 @@ readFromTTC loc reexp fname modNS importAs
ttc <- readTTCFile modNS as r bin
traverse (addGlobalDef modNS as) (context ttc)
setNS (currentNS ttc)
-- TODO: Set up typeHints and autoHints properly
resetFirstEntry
-- Finally, update the unification state with the holes from the

17
src/Core/CaseBuilder.idr
View File

@ -69,7 +69,7 @@ updatePats {todo = pvar :: ns} env (NBind fc _ (Pi c _ farg) fsc) (p :: ps)
do defs <- get Ctxt
empty <- clearDefs defs
pure (record { argType = Known c !(quote empty env farg) } p
:: !(updatePats env !(fsc (toClosure defaultOpts env (Ref fc Bound pvar))) ps))
:: !(updatePats env !(fsc defs (toClosure defaultOpts env (Ref fc Bound pvar))) ps))
_ => pure (p :: ps)
updatePats env nf (p :: ps)
= case argType p of
@ -98,7 +98,7 @@ substInPatInfo {pvar} {vars} fc n tm p ps
NBind pfc _ (Pi c _ farg) fsc =>
pure (record { argType = Known c !(quote empty env farg) } p,
!(updatePats env
!(fsc (toClosure defaultOpts env
!(fsc defs (toClosure defaultOpts env
(Ref pfc Bound pvar))) ps))
_ => pure (p, ps)
Unknown => pure (p, ps)
@ -335,10 +335,10 @@ nextNames {vars} fc root (p :: pats) fty
case fty of
Nothing => pure (Nothing, Unknown)
Just (NBind pfc _ (Pi c _ (NErased _)) fsc) =>
pure (Just !(fsc (toClosure defaultOpts env (Ref pfc Bound n))),
pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
Unknown)
Just (NBind pfc _ (Pi c _ farg) fsc) =>
pure (Just !(fsc (toClosure defaultOpts env (Ref pfc Bound n))),
pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
Known c !(quote empty env farg))
Just t =>
pure (Nothing, Stuck !(quote empty env t))
@ -404,8 +404,8 @@ groupCons fc fn pvars cs
addConG {todo} n tag pargs pats rhs []
= do cty <- the (Core (NF vars)) $if n == UN "->"
then pure $ NBind fc (MN "_" 0) (Pi RigW Explicit (NType fc)) $
const $ pure $ NBind fc (MN "_" 1) (Pi RigW Explicit (NErased fc)) $
const $ pure $ NType fc
(\d, a => pure $ NBind fc (MN "_" 1) (Pi RigW Explicit (NErased fc))
(\d, a => pure $ NType fc))
else do defs <- get Ctxt
Just t <- lookupTyExact n (gamma defs)
| Nothing => pure (NErased fc)
@ -756,7 +756,7 @@ mkPatClause fc fn args ty (ps, rhs)
case fty of
Nothing => pure (Nothing, Unknown)
Just (NBind pfc _ (Pi c _ farg) fsc) =>
pure (Just !(fsc (toClosure defaultOpts [] (Ref pfc Bound arg))),
pure (Just !(fsc defs (toClosure defaultOpts [] (Ref pfc Bound arg))),
Known c (embed {more = arg :: args}
!(quote empty [] farg)))
Just t =>
@ -830,7 +830,8 @@ getPMDef fc phase fn ty []
where
getArgs : Int -> NF [] -> Core (List Name)
getArgs i (NBind fc x (Pi _ _ _) sc)
= do sc' <- sc (toClosure defaultOpts [] (Erased fc))
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc))
pure (MN "arg" i :: !(getArgs i sc'))
getArgs i _ = pure []
getPMDef fc phase fn ty clauses

292
src/Core/Context.idr
View File

@ -7,13 +7,13 @@ import public Core.Name
import Core.Options
import public Core.TT
import Core.TTC
import Core.Value
import Utils.Binary
import Data.IOArray
import Data.NameMap
import Data.StringMap
import Data.IntMap
%default covering
@ -31,6 +31,12 @@ record Context a where
possibles : StringMap (List (Name, Int))
-- Reference to the actual content, indexed by Int
content : Ref Arr (IOArray a)
-- Branching depth, in a backtracking elaborator. 0 is top level; at lower
-- levels we need to stage updates rather than add directly to the
-- 'content' store
branchDepth : Nat
-- Things which we're going to add, if this branch succeeds
staging : IntMap a
-- Namespaces which are visible (i.e. have been imported)
-- This only matters during evaluation and type checking, to control
@ -65,7 +71,7 @@ initCtxtS : Int -> Core (Context a)
initCtxtS s
= do arr <- coreLift $ newArray s
aref <- newRef Arr arr
pure (MkContext 0 0 empty empty aref [])
pure (MkContext 0 0 empty empty aref 0 empty [])
export
initCtxt : Core (Context a)
@ -111,38 +117,44 @@ getNameID n ctxt = lookup n (resolvedAs ctxt)
-- Add the name to the context, or update the existing entry if it's already
-- there.
-- If we're not at the top level, add it to the staging area
export
addCtxt : Name -> a -> Context a -> Core (Int, Context a)
addCtxt n val ctxt_in
= do (idx, ctxt) <- getPosition n ctxt_in
let a = content ctxt
arr <- get Arr
coreLift $ writeArray arr idx val
pure (idx, ctxt)
= if branchDepth ctxt_in == 0
then do (idx, ctxt) <- getPosition n ctxt_in
let a = content ctxt
arr <- get Arr
coreLift $ writeArray arr idx val
pure (idx, ctxt)
else do (idx, ctxt) <- getPosition n ctxt_in
pure (idx, record { staging $= insert idx val } ctxt)
export
lookupCtxtExactI : Name -> Context a -> Core (Maybe (Int, a))
lookupCtxtExactI (Resolved idx) ctxt
= do let a = content ctxt
arr <- get Arr
Just def <- coreLift (readArray arr idx)
| Nothing => pure Nothing
pure (Just (idx, def))
= case lookup idx (staging ctxt) of
Just val => pure (Just (idx, val))
Nothing =>
do let a = content ctxt
arr <- get Arr
Just def <- coreLift (readArray arr idx)
| Nothing => pure Nothing
pure (Just (idx, def))
lookupCtxtExactI n ctxt
= do let Just idx = lookup n (resolvedAs ctxt)
| Nothing => pure Nothing
let a = content ctxt
arr <- get Arr
Just def <- coreLift (readArray arr idx)
| Nothing => pure Nothing
pure (Just (idx, def))
lookupCtxtExactI (Resolved idx) ctxt
export
lookupCtxtExact : Name -> Context a -> Core (Maybe a)
lookupCtxtExact (Resolved idx) ctxt
= do let a = content ctxt
arr <- get Arr
coreLift (readArray arr idx)
= case lookup idx (staging ctxt) of
Just res => pure (Just res)
Nothing =>
do let a = content ctxt
arr <- get Arr
coreLift (readArray arr idx)
lookupCtxtExact n ctxt
= do Just (i, def) <- lookupCtxtExactI n ctxt
| Nothing => pure Nothing
@ -179,6 +191,29 @@ lookupCtxtName n ctxt
pure (r :: rs')
else getMatches rs
branchCtxt : Context a -> Core (Context a)
branchCtxt ctxt = pure (record { branchDepth $= S } ctxt)
commitCtxt : Context a -> Core (Context a)
commitCtxt ctxt
= case branchDepth ctxt of
Z => pure ctxt
S Z => -- add all the things from 'staging' to the real array
do let a = content ctxt
arr <- get Arr
coreLift $ commitStaged (toList (staging ctxt)) arr
pure (record { staging = empty,
branchDepth = Z } ctxt)
S k => pure (record { branchDepth = k } ctxt)
where
-- We know the array must be big enough, because it will have been resized
-- if necessary in the branch to fit the index we've been given here
commitStaged : List (Int, a) -> IOArray a -> IO ()
commitStaged [] arr = pure ()
commitStaged ((idx, val) :: rest) arr
= do writeArray arr idx val
commitStaged rest arr
public export
data Def : Type where
None : Def -- Not yet defined
@ -195,6 +230,7 @@ data Def : Type where
(parampos : List Nat) -> -- parameters
(detpos : List Nat) -> -- determining arguments
(datacons : List Name) ->
(typehints : List (Name, Bool)) ->
Def
Hole : (invertible : Bool) -> Def
-- Constraints are integer references into the current map of
@ -208,7 +244,7 @@ Show Def where
show (PMDef args ct rt pats)
= show args ++ "; " ++ show ct
show (DCon t a) = "DataCon " ++ show t ++ " " ++ show a
show (TCon t a ps ds cons)
show (TCon t a ps ds cons hints)
= "TyCon " ++ show t ++ " " ++ show a ++ " " ++ show cons
show (Hole inv) = "Hole"
show (Guess tm cs) = "Guess " ++ show tm ++ " when " ++ show cs
@ -220,7 +256,7 @@ TTC Def where
toBuf b (PMDef args ct rt pats)
= do tag 1; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats
toBuf b (DCon t arity) = do tag 2; toBuf b t; toBuf b arity
toBuf b (TCon t arity parampos detpos datacons)
toBuf b (TCon t arity parampos detpos datacons _)
= do tag 3; toBuf b t; toBuf b arity; toBuf b parampos
toBuf b detpos; toBuf b datacons
toBuf b (Hole invertible) = do tag 4; toBuf b invertible
@ -239,7 +275,7 @@ TTC Def where
pure (DCon t a)
3 => do t <- fromBuf r b; a <- fromBuf r b
ps <- fromBuf r b; dets <- fromBuf r b; cs <- fromBuf r b
pure (TCon t a ps dets cs)
pure (TCon t a ps dets cs [])
4 => do i <- fromBuf r b;
pure (Hole i)
5 => do g <- fromBuf r b; cs <- fromBuf r b
@ -270,9 +306,7 @@ data TotalReq = Total | CoveringOnly | PartialOK
public export
data DefFlag
= TypeHint Name Bool -- True == direct hint
| GlobalHint Bool -- True == always search (not a default hint)
| Inline
= Inline
| Invertible -- assume safe to cancel arguments in unification
| Overloadable -- allow ad-hoc overloads
| TCInline -- always inline before totality checking
@ -294,8 +328,6 @@ Eq TotalReq where
export
Eq DefFlag where
(==) (TypeHint ty x) (TypeHint ty' y) = ty == ty' && x == y
(==) (GlobalHint x) (GlobalHint y) = x == y
(==) Inline Inline = True
(==) Invertible Invertible = True
(==) Overloadable Overloadable = True
@ -316,8 +348,6 @@ TTC TotalReq where
_ => corrupt "TotalReq"
TTC DefFlag where
toBuf b (TypeHint x y) = do tag 0; toBuf b x; toBuf b y
toBuf b (GlobalHint t) = do tag 1; toBuf b t
toBuf b Inline = tag 2
toBuf b Invertible = tag 3
toBuf b Overloadable = tag 4
@ -326,8 +356,6 @@ TTC DefFlag where
fromBuf s b
= case !getTag of
0 => do x <- fromBuf s b; y <- fromBuf s b; pure (TypeHint x y)
1 => do t <- fromBuf s b; pure (GlobalHint t)
2 => pure Inline
3 => pure Invertible
4 => pure Overloadable
@ -384,15 +412,31 @@ record Defs where
options : Options
toSave : NameMap ()
nextTag : Int
autoHints : NameMap Bool
-- ^ global search hints. A mapping from the hint name, to whether it is
-- a "default hint". A default hint is used only if all other attempts
-- to search fail (this flag is really only intended as a mechanism
-- for defaulting of literals)
openHints : NameMap ()
-- ^ currently open global hints; just for the rest of this module (not exported)
-- and prioritised
typeHints : List (Name, Name, Bool)
-- ^ a mapping from type names to hints (and a flag setting whether it's
-- a "direct" hint). Direct hints are searched first (as part of a group)
-- the indirect hints. Indirect hints, in practice, are used to find
-- instances of parent interfaces, and we don't search these until we've
-- tried to find a direct result via a constructor or a top level hint.
-- We don't look up anything in here, it's merely for saving out to TTC.
-- We save the hints in the 'GlobalDef' itself for faster lookup.
ifaceHash : Int
-- interface hashes of imported modules
importHashes : List (List String, Int)
-- imported modules, whether to rexport, as namespace
-- ^ interface hashes of imported modules
imported : List (List String, Bool, List String)
-- all imported filenames/namespaces, just to avoid loading something
-- twice unnecessarily (this is a record of all the things we've
-- called 'readFromTTC' with, in practice)
-- ^ imported modules, whether to rexport, as namespace
allImported : List (String, List String)
-- ^ all imported filenames/namespaces, just to avoid loading something
-- twice unnecessarily (this is a record of all the things we've
-- called 'readFromTTC' with, in practice)
export
clearDefs : Defs -> Core Defs
@ -404,7 +448,8 @@ export
initDefs : Core Defs
initDefs
= do gam <- initCtxt
pure (MkDefs gam ["Main"] defaults empty 100 5381 [] [] [])
pure (MkDefs gam ["Main"] defaults empty 100
empty empty [] 5381 [] [] [])
-- Label for context references
export
@ -437,6 +482,31 @@ setCtxt gam
= do defs <- get Ctxt
put Ctxt (record { gamma = gam } defs)
-- Call this before trying alternative elaborations, so that updates to the
-- context are put in the staging area rather than writing over the mutable
-- array of definitions.
-- Returns the old context (the one we'll go back to if the branch fails)
export
branch : {auto c : Ref Ctxt Defs} ->
Core Defs
branch
= do ctxt <- get Ctxt
gam' <- branchCtxt (gamma ctxt)
setCtxt gam'
pure ctxt
-- Call this after trying an elaboration to commit any changes to the mutable
-- array of definitions once we know they're correct. Only actually commits
-- when we're right back at the top level
export
commit : {auto c : Ref Ctxt Defs} ->
Core ()
commit
= do ctxt <- get Ctxt
gam' <- commitCtxt (gamma ctxt)
setCtxt gam'
-- Get the names to save. These are the ones explicitly noted, and the
-- ones between firstEntry and nextEntry (which are the names introduced in
-- the current source file)
@ -502,6 +572,141 @@ export
lookupTyName : Name -> Context GlobalDef -> Core (List (Name, Int, ClosedTerm))
lookupTyName = lookupNameBy type
export
setFlag : {auto c : Ref Ctxt Defs} ->
FC -> Name -> DefFlag -> Core ()
setFlag fc n fl
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
let flags' = fl :: filter (/= fl) (flags def)
addDef n (record { flags = flags' } def)
pure ()
export
setNameFlag : {auto c : Ref Ctxt Defs} ->
FC -> Name -> DefFlag -> Core ()
setNameFlag fc n fl
= do defs <- get Ctxt
[(n', i, def)] <- lookupCtxtName n (gamma defs)
| [] => throw (UndefinedName fc n)
| res => throw (AmbiguousName fc (map fst res))
let flags' = fl :: filter (/= fl) (flags def)
addDef (Resolved i) (record { flags = flags' } def)
pure ()
export
unsetFlag : {auto c : Ref Ctxt Defs} ->
FC -> Name -> DefFlag -> Core ()
unsetFlag fc n fl
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
let flags' = filter (/= fl) (flags def)
addDef n (record { flags = flags' } def)
pure ()
export
hasFlag : {auto c : Ref Ctxt Defs} ->
FC -> Name -> DefFlag -> Core Bool
hasFlag fc n fl
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
pure (fl `elem` flags def)
public export
record SearchData where
constructor MkSearchData
detArgs : List Nat -- determining argument positions
hintGroups : List (List Name) -- names of functions to use as hints.
{- In proof search, for every group of names
* If exactly one succeeds, use it
* If more than one succeeds, report an ambiguity error
* If none succeed, move on to the next group
This allows us to prioritise some names (e.g. to declare 'open' hints,
which we might us to open an implementation working as a module, or to
declare a named implementation to be used globally), and to have names
which are only used if all else fails (e.g. as a defaulting mechanism),
while the proof search mechanism doesn't need to know about any of the
details.
-}
-- Get the auto search data for a name.
export
getSearchData : {auto c : Ref Ctxt Defs} ->
FC -> (defaults : Bool) -> Name ->
Core SearchData
getSearchData fc defaults target
= do defs <- get Ctxt
Just (TCon _ _ _ dets cons hs) <- lookupDefExact target (gamma defs)
| _ => throw (UndefinedName fc target)
if defaults
then let defaults = map fst (filter isDefault
(toList (autoHints defs))) in
pure (MkSearchData [] [defaults])
else let opens = map fst (toList (openHints defs))
autos = map fst (filter (not . isDefault)
(toList (autoHints defs)))
tyhs = map fst (filter direct hs)
chasers = map fst (filter (not . direct) hs) in
pure (MkSearchData dets (filter isCons
[opens, autos, tyhs, chasers]))
where
isDefault : (Name, Bool) -> Bool
isDefault = snd
direct : (Name, Bool) -> Bool
direct = snd
export
setDetermining : {auto c : Ref Ctxt Defs} ->
FC -> Name -> List Name -> Core ()
setDetermining fc tyn args
= do defs <- get Ctxt
Just g <- lookupCtxtExact tyn (gamma defs)
| _ => throw (UndefinedName fc tyn)
let TCon t a ps _ cons hs = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor"))
apos <- getPos 0 args (type g)
updateDef tyn (const (Just (TCon t a ps apos cons hs)))
where
-- Type isn't normalised, but the argument names refer to those given
-- explicitly in the type, so there's no need.
getPos : Nat -> List Name -> Term vs -> Core (List Nat)
getPos i ns (Bind _ x (Pi _ _ _) sc)
= if x `elem` ns
then do rest <- getPos (1 + i) (filter (/=x) ns) sc
pure $ i :: rest
else getPos (1 + i) ns sc
getPos _ [] _ = pure []
getPos _ ns ty = throw (GenericMsg fc ("Unknown determining arguments: "
++ showSep ", " (map show ns)))
export
addHintFor : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Name -> Bool -> Core ()
addHintFor fc tyn hintn direct
= do defs <- get Ctxt
Just (TCon t a ps dets cons hs) <- lookupDefExact tyn (gamma defs)
| _ => throw (GenericMsg fc (show tyn ++ " is not a type constructor"))
updateDef tyn (const (Just (TCon t a ps dets cons ((hintn, direct) :: hs))))
export
addGlobalHint : {auto c : Ref Ctxt Defs} ->
Name -> Bool -> Core ()
addGlobalHint hint isdef
= do d <- get Ctxt
put Ctxt (record { autoHints $= insert hint isdef } d)
export
addOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
addOpenHint hint
= do d <- get Ctxt
put Ctxt (record { openHints $= insert hint () } d)
-- Set the default namespace for new definitions
export
setNS : {auto c : Ref Ctxt Defs} ->
@ -538,7 +743,7 @@ addData vis (MkData (MkCon dfc tyn arity tycon) datacons)
(TCon tag arity
(paramPos tyn (map type datacons))
(allDet arity)
(map name datacons))
(map name datacons) [])
(idx, gam') <- addCtxt tyn tydef (gamma defs)
gam'' <- addDataConstructors 0 datacons gam'
put Ctxt (record { gamma = gam'' } defs)
@ -608,11 +813,14 @@ toFullNames tm
where
full : Context GlobalDef -> Term vars -> Core (Term vars)
full gam (Ref fc x (Resolved i))
= do let a = content gam
arr <- get Arr
Just gdef <- coreLift (readArray arr i)
= do Just gdef <- lookupCtxtExact (Resolved i) gam
| Nothing => pure (Ref fc x (Resolved i))
pure (Ref fc x (fullname gdef))
-- = do let a = content gam
-- arr <- get Arr
-- Just gdef <- coreLift (readArray arr i)
-- | Nothing => pure (Ref fc x (Resolved i))
-- pure (Ref fc x (fullname gdef))
full gam (Meta fc x y xs)
= pure (Meta fc x y !(traverse (full gam) xs))
full gam (Bind fc x b scope)

29
src/Core/Normalise.idr
View File

@ -14,15 +14,15 @@ import Core.Value
-- part will only be constructed when needed, because it's in Core.
public export
data Glued : List Name -> Type where
MkGlue : Core (Term vars) -> Core (NF vars) -> Glued vars
MkGlue : Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars
export
getTerm : Glued vars -> Core (Term vars)
getTerm (MkGlue tm _) = tm
export
getNF : Glued vars -> Core (NF vars)
getNF (MkGlue _ nf) = nf
getNF : {auto c : Ref Ctxt Defs} -> Glued vars -> Core (NF vars)
getNF {c} (MkGlue _ nf) = nf c
Stack : List Name -> Type
Stack vars = List (AppInfo, Closure vars)
@ -58,7 +58,8 @@ parameters (defs : Defs, opts : EvalOpts)
eval env locs (Bind fc x b scope) stk
= do b' <- traverse (\tm => eval env locs tm stk) b
pure $ NBind fc x b'
(\arg => eval env (arg :: locs) scope stk)
(\defs', arg => evalWithOpts defs' opts
env (arg :: locs) scope stk)
eval env locs (App fc fn p arg) stk
= eval env locs fn ((p, MkClosure opts locs env arg) :: stk)
eval env locs (As fc _ tm) stk = eval env locs tm stk
@ -93,7 +94,7 @@ parameters (defs : Defs, opts : EvalOpts)
where
applyToStack : NF free -> Stack free -> Core (NF free)
applyToStack (NBind fc _ (Lam r e ty) sc) ((p, arg) :: stk)
= do arg' <- sc arg
= do arg' <- sc defs arg
applyToStack arg' stk
applyToStack (NApp fc (NRef nt fn) args) stk
= evalRef {vars = xs} env locs False fc nt fn (args ++ stk)
@ -284,12 +285,14 @@ nfOpts : EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)
nfOpts opts defs env tm = eval defs opts env [] tm []
export
gnf : Defs -> Env Term vars -> Term vars -> Glued vars
gnf defs env tm = MkGlue (pure tm) (nf defs env tm)
gnf : Env Term vars -> Term vars -> Glued vars
gnf env tm = MkGlue (pure tm)
(\c => do defs <- get Ctxt
nf defs env tm)
export
gType : FC -> Glued vars
gType fc = MkGlue (pure (TType fc)) (pure (NType fc))
gType fc = MkGlue (pure (TType fc)) (const (pure (NType fc)))
export
data QVar : Type where
@ -383,7 +386,7 @@ mutual
quoteGenNF q defs bound env (NBind fc n b sc)
= do var <- genName "qv"
sc' <- quoteGenNF q defs (Add n var bound) env
!(sc (toClosure defaultOpts env (Ref fc Bound var)))
!(sc defs (toClosure defaultOpts env (Ref fc Bound var)))
b' <- quoteBinder q defs bound env b
pure (Bind fc n b' sc')
quoteGenNF q defs bound env (NApp fc f args)
@ -432,7 +435,7 @@ glueBack : Defs -> Env Term vars -> NF vars -> Glued vars
glueBack defs env nf
= MkGlue (do empty <- clearDefs defs
quote empty env nf)
(pure nf)
(const (pure nf))
export
normalise : Defs -> Env Term free -> Term free -> Core (Term free)
@ -501,8 +504,8 @@ mutual
let c = MkClosure defaultOpts [] env (Ref fc Bound var)
bok <- convBinders q defs env b b'
if bok
then do bsc <- sc c
bsc' <- sc' c
then do bsc <- sc defs c
bsc' <- sc' defs c
convGen q defs env bsc bsc'
else pure False
@ -565,7 +568,7 @@ mutual
export
getValArity : Defs -> Env Term vars -> NF vars -> Core Nat
getValArity defs env (NBind fc x (Pi _ _ _) sc)
= pure (S !(getValArity defs env !(sc (toClosure defaultOpts env (Erased fc)))))
= pure (S !(getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc)))))
getValArity defs env val = pure 0
export

40
src/Core/Unify.idr
View File

@ -244,9 +244,10 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
Just rhs =>
do logTerm 5 ("Instantiated: " ++ show mname) ty
logTerm 5 "Definition" rhs
noteUpdate mref
addDef (Resolved mref)
(record { definition = PMDef [] (STerm rhs) (STerm rhs) [] } mdef)
let newdef = record { definition =
PMDef [] (STerm rhs) (STerm rhs) []
} mdef
addDef (Resolved mref) newdef
removeHole mref
where
updateLoc : {v : Nat} -> List (Var vs) -> .(IsVar name v vs') ->
@ -491,8 +492,10 @@ mutual
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyMode -> FC -> Env Term vars ->
FC -> Name -> Binder (NF vars) -> (Closure vars -> Core (NF vars)) ->
FC -> Name -> Binder (NF vars) -> (Closure vars -> Core (NF vars)) ->
FC -> Name -> Binder (NF vars) ->
(Defs -> Closure vars -> Core (NF vars)) ->
FC -> Name -> Binder (NF vars) ->
(Defs -> Closure vars -> Core (NF vars)) ->
Core UnifyResult
unifyBothBinders mode loc env xfc x (Pi cx ix tx) scx yfc y (Pi cy iy ty) scy
= do defs <- get Ctxt
@ -511,8 +514,8 @@ mutual
= Pi cx ix tx' :: env
case constraints ct of
[] => -- No constraints, check the scope
do tscx <- scx (toClosure defaultOpts env (Ref loc Bound xn))
tscy <- scy (toClosure defaultOpts env (Ref loc Bound xn))
do tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
tmx <- quote empty env tscx
tmy <- quote empty env tscy
unify mode loc env' (refsToLocals (Add x xn None) tmx)
@ -524,8 +527,8 @@ mutual
(Bind xfc x (Lam cx Explicit txtm) (Local xfc Nothing _ First))
(Bind xfc x (Pi cx Explicit txtm)
(weaken tytm)) cs
tscx <- scx (toClosure defaultOpts env (Ref loc Bound xn))
tscy <- scy (toClosure defaultOpts env (App loc c (explApp Nothing) (Ref loc Bound xn)))
tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
tscy <- scy defs (toClosure defaultOpts env (App loc c (explApp Nothing) (Ref loc Bound xn)))
tmx <- quote empty env tscx
tmy <- quote empty env tscy
cs' <- unify mode loc env' (refsToLocals (Add x xn None) tmx)
@ -552,18 +555,17 @@ mutual
(NDCon xfc x tagx ax xs)
(NDCon yfc y tagy ay ys)
unifyNoEta mode loc env (NTCon xfc x tagx ax xs) (NTCon yfc y tagy ay ys)
= do gam <- get Ctxt
if x == y
then unifyArgs mode loc env (map snd xs) (map snd ys)
= if x == y
then unifyArgs mode loc env (map snd xs) (map snd ys)
-- TODO: Type constructors are not necessarily injective.
-- If we don't know it's injective, need to postpone the
-- constraint. But before then, we need some way to decide
-- what's injective...
-- then postpone loc env (quote empty env (NTCon x tagx ax xs))
-- (quote empty env (NTCon y tagy ay ys))
else convertError loc env
(NTCon xfc x tagx ax xs)
(NTCon yfc y tagy ay ys)
else convertError loc env
(NTCon xfc x tagx ax xs)
(NTCon yfc y tagy ay ys)
unifyNoEta mode loc env (NApp xfc fx axs) (NApp yfc fy ays)
= unifyBothApps mode loc env xfc fx axs yfc fy ays
@ -586,12 +588,12 @@ mutual
export
Unify Term where
unifyD _ _ mode loc env x y
= do gam <- get Ctxt
if !(convert gam env x y)
= do defs <- get Ctxt
if !(convert defs env x y)
then do log 10 $ "Skipped unification (convert already): "
++ show x ++ " and " ++ show y
pure success
else unify mode loc env !(nf gam env x) !(nf gam env y)
else unify mode loc env !(nf defs env x) !(nf defs env y)
export
Unify Closure where
@ -650,12 +652,10 @@ retryGuess mode smode (hid, (loc, hname))
-- hole list
[] => do let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def
logTerm 5 ("Resolved " ++ show hname) tm
noteUpdate hid
addDef (Resolved hid) gdef
removeGuess hid
pure (holesSolved csAll)
newcs => do let gdef = record { definition = Guess tm newcs } def
noteUpdate hid
addDef (Resolved hid) gdef
pure False
_ => pure False

48
src/Core/UnifyState.idr
View File

@ -65,15 +65,10 @@ record UState where
constraints : IntMap Constraint -- map for finding constraints by ID
nextName : Int
nextConstraint : Int
updateLog : Maybe (List (Int, GlobalDef))
-- List of updates made to definitions in this branch of
-- elaboration, which we'll need to undo if we backtrack.
-- This will be a performance penalty in backtracking so
-- we should avoid it as far as we can!
export
initUState : UState
initUState = MkUState empty empty empty empty 0 0 Nothing
initUState = MkUState empty empty empty empty 0 0
export
data UST : Type where
@ -164,21 +159,6 @@ removeGuess n
= do ust <- get UST
put UST (record { guesses $= delete n } ust)
export
noteUpdate : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Int -> Core ()
noteUpdate i
= do ust <- get UST
case updateLog ust of
Nothing => pure ()
Just ups =>
do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => pure ()
put UST (record { updateLog = Just ((i, gdef) :: ups) }
ust)
-- Get all of the hole data
export
getHoles : {auto u : Ref UST UState} ->
@ -326,22 +306,13 @@ tryErrorUnify : {auto c : Ref Ctxt Defs} ->
Core a -> Core (Either Error a)
tryErrorUnify elab
= do ust <- get UST
next <- getNextEntry
let btlog = updateLog ust
put UST (record { updateLog = Just [] } ust)
defs <- branch
catch (do res <- elab
commit
pure (Right res))
(\err => do ust' <- get UST
maybe (pure ()) undoLog (updateLog ust')
put UST ust
setNextEntry next
(\err => do put UST ust
put Ctxt defs
pure (Left err))
where
undoLog : List (Int, GlobalDef) -> Core ()
undoLog [] = pure ()
undoLog ((i, d) :: rest)
= do addDef (Resolved i) d
undoLog rest
export
tryUnify : {auto c : Ref Ctxt Defs} ->
@ -352,6 +323,15 @@ tryUnify elab1 elab2
| Left err => elab2
pure ok
export
handleUnify : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Core a -> (Error -> Core a) -> Core a
handleUnify elab1 elab2
= do Right ok <- tryErrorUnify elab1
| Left err => elab2 err
pure ok
-- A hole is 'valid' - i.e. okay to leave unsolved for later - as long as it's
-- not guarded by a unification problem (in which case, report that the unification
-- problem is unsolved) and it doesn't depend on an implicit pattern variable

3
src/Core/Value.idr
View File

@ -1,5 +1,6 @@
module Core.Value
import Core.Context
import Core.Core
import Core.Env
import Core.TT
@ -47,7 +48,7 @@ mutual
public export
data NF : List Name -> Type where
NBind : FC -> (x : Name) -> Binder (NF vars) ->
(Closure vars -> Core (NF vars)) -> NF vars
(Defs -> Closure vars -> Core (NF vars)) -> NF vars
NApp : FC -> NHead vars -> List (AppInfo, Closure vars) -> NF vars
NDCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
List (AppInfo, Closure vars) -> NF vars

63
src/TTImp/Elab/App.idr
View File

@ -23,9 +23,8 @@ getNameType rigc env fc x expected
= case defined x env of
Just (MkIsDefined rigb lv) =>
do rigSafe rigb rigc
defs <- get Ctxt
let bty = binderType (getBinder lv env)
pure (Local fc (Just rigb) _ lv, gnf defs env bty)
pure (Local fc (Just rigb) _ lv, gnf env bty)
Nothing =>
do defs <- get Ctxt
[(fullname, i, def)] <- lookupCtxtName x (gamma defs)
@ -34,9 +33,9 @@ getNameType rigc env fc x expected
let nt = case definition def of
PMDef _ _ _ _ => Func
DCon t a => DataCon t a
TCon t a _ _ _ => TyCon t a
TCon t a _ _ _ _ => TyCon t a
_ => Func
pure (Ref fc nt (Resolved i), gnf defs env (embed (type def)))
pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
where
rigSafe : RigCount -> RigCount -> Core ()
rigSafe Rig1 RigW = throw (LinearMisuse fc x Rig1 RigW)
@ -51,14 +50,14 @@ isHole _ = False
-- Return whether we already know the return type of the given function
-- type. If we know this, we can possibly infer some argument types before
-- elaborating them, which might help us disambiguate things more easily.
concrete : Env Term vars -> NF vars -> Core Bool
concrete env (NBind fc _ (Pi _ _ _) sc)
= do sc' <- sc (toClosure defaultOpts env (Erased fc))
concrete env sc'
concrete env (NDCon _ _ _ _ _) = pure True
concrete env (NTCon _ _ _ _ _) = pure True
concrete env (NPrimVal _ _) = pure True
concrete env _ = pure False
concrete : Defs -> Env Term vars -> NF vars -> Core Bool
concrete defs env (NBind fc _ (Pi _ _ _) sc)
= do sc' <- sc defs (toClosure defaultOpts env (Erased fc))
concrete defs env sc'
concrete defs env (NDCon _ _ _ _ _) = pure True
concrete defs env (NTCon _ _ _ _ _) = pure True
concrete defs env (NPrimVal _ _) = pure True
concrete defs env _ = pure False
mutual
makeImplicit : {vars : _} ->
@ -67,7 +66,7 @@ mutual
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo -> Env Term vars ->
FC -> (fntm : Term vars) ->
Name -> NF vars -> (Closure vars -> Core (NF vars)) ->
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(knownret : Bool) ->
@ -80,7 +79,7 @@ mutual
metaty <- quote empty env aty
metaval <- metaVar fc rig env nm metaty
let fntm = App fc tm (appInf (Just x) Implicit) metaval
fnty <- sc (toClosure defaultOpts env metaval)
fnty <- sc defs (toClosure defaultOpts env metaval)
when (bindingVars elabinfo) $
do est <- get EST
put EST (addBindIfUnsolved nm rig env metaval metaty est)
@ -93,7 +92,7 @@ mutual
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo -> Env Term vars ->
FC -> (fntm : Term vars) ->
Name -> NF vars -> (Closure vars -> Core (NF vars)) ->
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(knownret : Bool) ->
@ -113,7 +112,7 @@ mutual
{auto e : Ref EST (EState vars)} ->
RigCount -> RigCount -> ElabInfo -> Env Term vars ->
FC -> AppInfo -> (fntm : Term vars) -> Name ->
(aty : NF vars) -> (sc : Closure vars -> Core (NF vars)) ->
(aty : NF vars) -> (sc : Defs -> Closure vars -> Core (NF vars)) ->
(arg : RawImp) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
@ -122,19 +121,19 @@ mutual
Core (Term vars, Glued vars)
checkRestApp rig argRig elabinfo env fc appinf tm x aty sc
arg expargs impargs knownret expty
= do kr <- if knownret
= do defs <- get Ctxt
kr <- if knownret
then pure True
else do sc' <- sc (toClosure defaultOpts env (Erased fc))
concrete env sc'
else do sc' <- sc defs (toClosure defaultOpts env (Erased fc))
concrete defs env sc'
if kr then do
defs <- get Ctxt
nm <- genMVName x
empty <- clearDefs defs
metaty <- quote empty env aty
metaval <- metaVar fc argRig env nm metaty
let fntm = App fc tm appinf metaval
logNF 10 ("Delaying " ++ show nm ++ " " ++ show arg) env aty
fnty <- sc (toClosure defaultOpts env metaval)
fnty <- sc defs (toClosure defaultOpts env metaval)
(tm, gty) <- checkAppWith rig elabinfo env fc
fntm fnty expargs impargs kr expty
defs <- get Ctxt
@ -143,24 +142,24 @@ mutual
(argv, argt) <- check argRig (nextLevel elabinfo)
env arg (Just (glueBack defs env aty'))
defs <- get Ctxt
[] <- convert fc elabinfo env (gnf defs env metaval)
(gnf defs env argv)
[] <- convert fc elabinfo env (gnf env metaval)
(gnf env argv)
| cs => throw (CantConvert fc env metaval argv)
removeHoleName nm
pure (tm, gty)
else do
defs <- get Ctxt
logNF 10 ("Argument type " ++ show x) env aty
logNF 10 ("Full function type") env
(NBind fc x (Pi argRig Explicit aty) sc)
logC 10 (do ety <- maybe (pure Nothing)
(\t => pure (Just !(toFullNames!(getTerm t))))
expty
(\t => pure (Just !(toFullNames!(getTerm t))))
expty
pure ("Overall expected type: " ++ show ety))
(argv, argt) <- check argRig (nextLevel elabinfo)
env arg (Just (glueBack defs env aty))
defs <- get Ctxt
let fntm = App fc tm appinf argv
fnty <- sc (toClosure defaultOpts env argv)
fnty <- sc defs (toClosure defaultOpts env argv)
checkAppWith rig elabinfo env fc
fntm fnty expargs impargs kr expty
@ -256,11 +255,12 @@ mutual
checkAppWith {vars} rig elabinfo env fc tm ty (arg :: expargs) impargs kr expty
= -- Invent a function type, and hope that we'll know enough to solve it
-- later when we unify with expty
do argn <- genName "argTy"
do logNF 10 "Function type" env ty
logTerm 10 "Function " tm
argn <- genName "argTy"
retn <- genName "retTy"
argTy <- metaVar fc Rig0 env argn (TType fc)
defs <- get Ctxt
let argTyG = gnf defs env argTy
let argTyG = gnf env argTy
-- Can't use 'metaVar' to record it for binding because it's
-- in a different scope... so it'll stay global
(_, retTy) <- newMeta {vars = argn :: vars}
@ -269,7 +269,10 @@ mutual
(argv, argt) <- check rig (nextLevel elabinfo)
env arg (Just argTyG)
let fntm = App fc tm (appInf Nothing Explicit) argv
defs <- get Ctxt
fnty <- nf defs env (Bind fc argn (Let RigW argv argTy) retTy)
logNF 10 "Function type" env fnty
maybe (pure ()) (logGlue 10 "Expected type" env) expty
checkAppWith rig elabinfo env fc fntm fnty expargs impargs kr expty
export

9
src/TTImp/Elab/Binders.idr
View File

@ -59,10 +59,9 @@ inferLambda rig elabinfo env fc rigl info n argTy scope expTy
let env' : Env Term (n :: _) = Lam rigb info tyv :: env
(scopev, scopet) <- inScope fc env' (\e' =>
check {e=e'} rig (nextLevel elabinfo) env' scope Nothing)
defs <- get Ctxt
checkExp rig elabinfo env fc
(Bind fc n (Lam rigb info tyv) scopev)
(gnf defs env
(gnf env
(Bind fc n (Pi rigb info tyv) !(getTerm scopet)))
Nothing
@ -102,11 +101,11 @@ checkLambda rig_in elabinfo env fc rigl info n argTy scope (Just expty_in)
(scopev, scopet) <-
inScope fc env' (\e' =>
check {e=e'} rig (nextLevel elabinfo) env' scope
(Just (gnf defs env' (renameTop n psc))))
(Just (gnf env' (renameTop n psc))))
checkExp rig elabinfo env fc
(Bind fc n (Lam rigb info tyv) scopev)
(gnf defs env
(gnf env
(Bind fc n (Pi rigb info tyv) !(getTerm scopet)))
(Just (gnf defs env
(Just (gnf env
(Bind fc bn (Pi rigb info pty) psc)))
_ => inferLambda rig elabinfo env fc rigl info n argTy scope (Just expty_in)

17
src/TTImp/Elab/Check.idr
View File

@ -221,23 +221,14 @@ tryError : {vars : _} ->
tryError elab
= do ust <- get UST
est <- get EST
next <- getNextEntry
let btlog = updateLog ust
put UST (record { updateLog = Just [] } ust)
defs <- branch
catch (do res <- elab
commit
pure (Right res))
(\err => do ust' <- get UST
maybe (pure ()) undoLog (updateLog ust')
put UST ust
(\err => do put UST ust
put EST est
setNextEntry next
put Ctxt defs
pure (Left err))
where
undoLog : List (Int, GlobalDef) -> Core ()
undoLog [] = pure ()
undoLog ((i, d) :: rest)
= do addDef (Resolved i) d
undoLog rest
export
try : {vars : _} ->

6
src/TTImp/Elab/ImplicitBind.idr
View File

@ -414,11 +414,11 @@ checkBindVar rig elabinfo env fc str topexp
(record { boundNames $= ((n, (tm, exp)) ::),
toBind $= ((n, (tm, bty)) :: ) } est)
-- addNameType loc (UN str) env exp
checkExp rig elabinfo env fc tm (gnf defs env exp) topexp
checkExp rig elabinfo env fc tm (gnf env exp) topexp
Just (tm, ty) =>
do -- TODO: for metadata addNameType loc (UN str) env ty
defs <- get Ctxt
checkExp rig elabinfo env fc tm (gnf defs env ty) topexp
checkExp rig elabinfo env fc tm (gnf env ty) topexp
export
checkBindHere : {vars : _} ->
@ -457,4 +457,4 @@ checkBindHere rig elabinfo env fc bindmode tm exp
!(normaliseHoles defs env tmv)
!(normaliseHoles defs env ty)
traverse implicitBind (map fst argImps)
checkExp rig elabinfo env fc bv (gnf defs env bt) exp
checkExp rig elabinfo env fc bv (gnf env bt) exp

11
src/TTImp/Elab/Term.idr
View File

@ -47,8 +47,9 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamNF tm@(ILam _ _ Implicit _ _ _) (NBind fc n (Pi _ Implicit _) sc)
= pure tm
bindLamNF tm (NBind fc n (Pi c Implicit ty) sc)
= do n' <- genVarName ("imp_" ++ show n)
sctm <- sc (toClosure defaultOpts env (Ref fc Bound n'))
= do defs <- get Ctxt
n' <- genVarName ("imp_" ++ show n)
sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
sc' <- bindLamNF tm sctm
pure $ ILam fc c Implicit (Just n') (Implicit fc False) sc'
bindLamNF tm sc = pure tm
@ -105,8 +106,7 @@ checkTerm rig elabinfo env (IMustUnify fc n tm) exp
checkTerm {vars} rig elabinfo env (IPrimVal fc c) exp
= do let (cval, cty) = checkPrim {vars} fc c
defs <- get Ctxt
checkExp rig elabinfo env fc cval (gnf defs env cty) exp
checkExp rig elabinfo env fc cval (gnf env cty) exp
checkTerm rig elabinfo env (IType fc) exp
= checkExp rig elabinfo env fc (TType fc) (gType fc) exp
@ -129,8 +129,7 @@ checkTerm rig elabinfo env (Implicit fc b) Nothing
when (b && bindingVars elabinfo) $
do est <- get EST
put EST (addBindIfUnsolved nm rig env metaval ty est)
defs <- get Ctxt
pure (metaval, gnf defs env ty)
pure (metaval, gnf env ty)
-- Declared in TTImp.Elab.Check
TTImp.Elab.Check.check rigc elabinfo env tm exp

36
src/TTImp/ProcessData.idr
View File

@ -11,20 +11,31 @@ import TTImp.Elab.Check
import TTImp.Elab
import TTImp.TTImp
checkRetType : Env Term vars -> NF vars ->
processDataOpt : {auto c : Ref Ctxt Defs} ->
FC -> Name -> DataOpt -> Core ()
processDataOpt fc n NoHints
= pure ()
processDataOpt fc ndef (SearchBy dets)
= setDetermining fc ndef dets
checkRetType : {auto c : Ref Ctxt Defs} ->
Env Term vars -> NF vars ->
(NF vars -> Core ()) -> Core ()
checkRetType env (NBind fc x (Pi _ _ ty) sc) chk
= checkRetType env !(sc (toClosure defaultOpts env (Erased fc))) chk
= do defs <- get Ctxt
checkRetType env !(sc defs (toClosure defaultOpts env (Erased fc))) chk
checkRetType env nf chk = chk nf
checkIsType : FC -> Name -> Env Term vars -> NF vars -> Core ()
checkIsType : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Env Term vars -> NF vars -> Core ()
checkIsType loc n env nf
= checkRetType env nf
(\nf => case nf of
NType _ => pure ()
_ => throw (BadTypeConType loc n))
checkFamily : FC -> Name -> Name -> Env Term vars -> NF vars -> Core ()
checkFamily : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Name -> Env Term vars -> NF vars -> Core ()
checkFamily loc cn tn env nf
= checkRetType env nf
(\nf => case nf of
@ -56,6 +67,9 @@ checkCon env vis tn (MkImpTy fc cn_in ty_raw)
pure (MkCon fc cn !(getArity defs [] fullty) fullty)
conName : Constructor -> Name
conName (MkCon _ cn _ _) = cn
export
processData : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -79,7 +93,7 @@ processData env fc vis (MkImpLater dfc n_in ty_raw)
-- Add the type constructor as a placeholder while checking
-- data constructors
tidx <- addDef n (newDef fc n Rig1 fullty vis
(TCon 0 arity [] [] []))
(TCon 0 arity [] [] [] []))
pure ()
processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
= do n <- inCurrentNS n_in
@ -96,7 +110,7 @@ processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
Nothing => pure ()
Just ndef =>
case definition ndef of
TCon _ _ _ _ _ =>
TCon _ _ _ _ _ _ =>
do ok <- convert defs [] fullty (type ndef)
if ok then pure ()
else throw (AlreadyDefined fc n)
@ -110,7 +124,7 @@ processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
-- Add the type constructor as a placeholder while checking
-- data constructors
tidx <- addDef n (newDef fc n Rig1 fullty vis
(TCon 0 arity [] [] []))
(TCon 0 arity [] [] [] []))
-- Constructors are private if the data type as a whole is
-- export
@ -120,6 +134,12 @@ processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
let ddef = MkData (MkCon dfc n arity fullty) cons
addData vis ddef
-- TODO: Interface hash, process options
traverse (processDataOpt fc (Resolved tidx)) opts
when (not (NoHints `elem` opts)) $
do traverse (\x => addHintFor fc n x True) (map conName cons)
pure ()
-- TODO: Interface hash
pure ()

21
src/TTImp/ProcessDef.idr
View File

@ -57,15 +57,17 @@ findLinear top bound rig tm
findLinArg : RigCount -> NF [] -> List (Term vars) ->
Core (List (Name, RigCount))
findLinArg rig (NBind _ x (Pi c _ _) sc) (Local {name=a} fc _ idx prf :: as)
= if idx < bound
then do sc' <- sc (toClosure defaultOpts [] (Ref fc Bound x))
pure $ (a, rigMult c rig) ::
!(findLinArg rig sc' as)
else do sc' <- sc (toClosure defaultOpts [] (Ref fc Bound x))
findLinArg rig sc' as
= do defs <- get Ctxt
if idx < bound
then do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))
pure $ (a, rigMult c rig) ::
!(findLinArg rig sc' as)
else do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))
findLinArg rig sc' as
findLinArg rig (NBind fc x (Pi c _ _) sc) (a :: as)
= pure $ !(findLinear False bound (rigMult c rig) a) ++
!(findLinArg rig !(sc (toClosure defaultOpts [] (Ref fc Bound x))) as)
= do defs <- get Ctxt
pure $ !(findLinear False bound (rigMult c rig) a) ++
!(findLinArg rig !(sc defs (toClosure defaultOpts [] (Ref fc Bound x))) as)
findLinArg rig ty (a :: as)
= pure $ !(findLinear False bound rig a) ++ !(findLinArg rig ty as)
findLinArg _ _ [] = pure []
@ -152,8 +154,7 @@ checkClause mult hashit n env (PatClause fc lhs_in rhs)
(vars' ** (env', lhstm', lhsty')) <-
extendEnv env lhstm_lin lhsty_lin
defs <- get Ctxt
rhstm <- checkTerm n InExpr env' rhs (gnf defs env' lhsty')
rhstm <- checkTerm n InExpr env' rhs (gnf env' lhsty')
logTermNF 5 "RHS term" env' rhstm
pure (Just (MkClause env' lhstm' rhstm))

2
src/Yaffle/REPL.idr
View File

@ -47,7 +47,7 @@ process (ProofSearch n_in)
[(n, i, ty)] <- lookupTyName n_in (gamma defs)
| [] => throw (UndefinedName toplevelFC n_in)
| ns => throw (AmbiguousName toplevelFC (map fst ns))
def <- search toplevelFC RigW n ty []
def <- search toplevelFC RigW False 1000 n ty []
defs <- get Ctxt
defnf <- normaliseHoles defs [] def
coreLift (printLn !(toFullNames defnf))