edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-23 04:42:05 +03:00
Code Issues Projects Releases Wiki Activity

Implement laziness

Browse Source 
Slight change of plan: instead of having special names, add Lazy, Inf,
Delay and Force and keywords and elaborate them specially.
Correspondingly, add DelayCase for case trees. Given that implicit
laziness is important, it seems better to do it this way than constantly
check whether the name we're working with is important.

This turns out to make implicit laziness much easier, because the
unifier can flag whether it had to go under a 'Delayed' to succeed, and
report that back to the elaborator which can then insert the necessary
coercion.
This commit is contained in:
Edwin Brady 2019-05-22 19:42:43 +01:00
parent 9f4ca9e67f
commit c75569c255
32 changed files with 530 additions and 204 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Core/Binary.idr
View File

@ -55,7 +55,6 @@ record TTCFile extra where
imported : List (List String, Bool, List String)
nextVar : Int
currentNS : List String
laziness : Maybe LazyNames
pairnames : Maybe PairNames
rewritenames : Maybe RewriteNames
primnames : PrimNames
@ -115,7 +114,6 @@ writeTTCFile b file
toBuf b (imported file)
toBuf b (nextVar file)
toBuf b (currentNS file)
toBuf b (laziness file)
toBuf b (pairnames file)
toBuf b (rewritenames file)
toBuf b (primnames file)
@ -151,7 +149,6 @@ readTTCFile modns as r b
imp <- fromBuf r b
nextv <- fromBuf r b
cns <- fromBuf r b
lz <- fromBuf r b
pns <- fromBuf r b
rws <- fromBuf r b
prims <- fromBuf r b
@ -160,7 +157,7 @@ readTTCFile modns as r b
pure (MkTTCFile ver ifaceHash importHashes r
holes guesses constraints defs
autohs typehs imp nextv cns
lz pns rws prims nds ex)
pns rws prims nds ex)
-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : List Name -> List GlobalDef -> Defs -> Core (List GlobalDef)
@ -200,7 +197,6 @@ writeToTTC extradata fname
(imported defs)
(nextName ust)
(currentNS defs)
(laziness (options defs))
(pairnames (options defs))
(rewritenames (options defs))
(primnames (options defs))
@ -252,6 +248,7 @@ readFromTTC loc reexp fname modNS importAs
traverse (addGlobalDef modNS as) (context ttc)
setNS (currentNS ttc)
-- TODO: Set up typeHints and autoHints properly
-- TODO: Set up pair/rewrite etc names, name directives
resetFirstEntry
-- Finally, update the unification state with the holes from the

74
src/Core/CaseBuilder.idr
View File

@ -214,6 +214,7 @@ namesIn pvars (PAs _ n p) = (n `elem` pvars) && namesIn pvars p
namesIn pvars (PCon _ _ _ _ ps) = all (namesIn pvars) ps
namesIn pvars (PTyCon _ _ _ ps) = all (namesIn pvars) ps
namesIn pvars (PArrow _ _ s t) = namesIn pvars s && namesIn pvars t
namesIn pvars (PDelay _ _ t p) = namesIn pvars t && namesIn pvars p
namesIn pvars (PLoc _ n) = n `elem` pvars
namesIn pvars _ = True
@ -222,6 +223,7 @@ namesFrom (PAs _ n p) = n :: namesFrom p
namesFrom (PCon _ _ _ _ ps) = concatMap namesFrom ps
namesFrom (PTyCon _ _ _ ps) = concatMap namesFrom ps
namesFrom (PArrow _ _ s t) = namesFrom s ++ namesFrom t
namesFrom (PDelay _ _ t p) = namesFrom t ++ namesFrom p
namesFrom (PLoc _ n) = [n]
namesFrom _ = []
@ -244,6 +246,7 @@ clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) rhs)
getClauseType phase (PTyCon _ _ _ xs) _ = ConClause
getClauseType phase (PConst _ x) _ = ConClause
getClauseType phase (PArrow _ _ s t) _ = ConClause
getClauseType phase (PDelay _ _ _ _) t = ConClause
getClauseType phase _ _ = VarClause
partition : Phase -> (ps : List (PatClause vars (a :: as))) -> Partitions ps
@ -264,6 +267,7 @@ partition phase (x :: xs) with (partition phase xs)
data ConType : Type where
CName : Name -> (tag : Int) -> ConType
CDelay : ConType
CConst : Constant -> ConType
conTypeEq : (x, y : ConType) -> Maybe (x = y)
@ -272,12 +276,12 @@ conTypeEq (CName x tag) (CName x' tag')
case decEq tag tag' of
Yes Refl => Just Refl
No contra => Nothing
conTypeEq (CName x tag) (CConst y) = Nothing
conTypeEq (CConst x) (CName y tag) = Nothing
conTypeEq CDelay CDelay = Just Refl
conTypeEq (CConst x) (CConst y)
= case constantEq x y of
Nothing => Nothing
Just Refl => Just Refl
conTypeEq _ _ = Nothing
data Group : List Name -> -- variables in scope
List Name -> -- pattern variables still to process
@ -285,17 +289,23 @@ data Group : List Name -> -- variables in scope
ConGroup : Name -> (tag : Int) ->
List (PatClause (newargs ++ vars) (newargs ++ todo)) ->
Group vars todo
DelayGroup : List (PatClause (tyarg :: valarg :: vars)
(tyarg :: valarg :: todo)) ->
Group vars todo
ConstGroup : Constant -> List (PatClause vars todo) ->
Group vars todo
Show (Group vars todo) where
show (ConGroup c t cs) = "Con " ++ show c ++ ": " ++ show cs
show (DelayGroup cs) = "Delay: " ++ show cs
show (ConstGroup c cs) = "Const " ++ show c ++ ": " ++ show cs
data GroupMatch : ConType -> List Pat -> Group vars todo -> Type where
ConMatch : LengthMatch ps newargs ->
GroupMatch (CName n tag) ps
(ConGroup {newargs} n tag (MkPatClause pvs pats rhs :: rest))
DelayMatch : GroupMatch CDelay []
(DelayGroup {tyarg} {valarg} (MkPatClause pvs pats rhs :: rest))
ConstMatch : GroupMatch (CConst c) []
(ConstGroup c (MkPatClause pvs pats rhs :: rest))
NoMatch : GroupMatch ct ps g
@ -308,8 +318,9 @@ checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pa
Just prf => case (nameEq x x', decEq tag tag') of
(Just Refl, Yes Refl) => ConMatch prf
_ => NoMatch
checkGroupMatch (CName x tag) ps (ConstGroup _ xs) = NoMatch
checkGroupMatch (CConst x) ps (ConGroup _ _ xs) = NoMatch
checkGroupMatch (CName x tag) ps _ = NoMatch
checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats rhs :: rest))
= DelayMatch
checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats rhs :: rest))
= case constantEq c c' of
Nothing => NoMatch
@ -381,6 +392,7 @@ updatePatNames ns (pi :: ps)
update (PCon fc n i a ps) = PCon fc n i a (map update ps)
update (PTyCon fc n a ps) = PTyCon fc n a (map update ps)
update (PArrow fc x s t) = PArrow fc x (update s) (update t)
update (PDelay fc r t p) = PDelay fc r (update t) (update p)
update (PLoc fc n)
= case lookup n ns of
Nothing => PLoc fc n
@ -443,6 +455,48 @@ groupCons fc fn pvars cs
= do gs' <- addConG n tag pargs pats rhs gs
pure (g :: gs')
-- This rather ugly special case is to deal with laziness, where Delay
-- is like a constructor, but with a special meaning that it forces
-- evaluation when case analysis reaches it (dealt with in the evaluator
-- and compiler)
addDelayG : Pat -> Pat -> NamedPats vars todo ->
(rhs : Term vars) ->
(acc : List (Group vars todo)) ->
Core (List (Group vars todo))
addDelayG {todo} pty parg pats rhs []
= do let dty = NBind fc (MN "a" 0) (Pi Rig0 Explicit (NType fc)) $
(\d, a =>
do a' <- evalClosure d a
pure (NBind fc (MN "x" 0) (Pi RigW Explicit a')
(\dv, av => pure (NDelayed fc LUnknown a'))))
([tyname, argname] ** newargs) <- nextNames {vars} fc "e" [pty, parg]
(Just dty)
| _ => throw (InternalError "Error compiling Delay pattern match")
let pats' = updatePatNames (updateNames [(tyname, pty),
(argname, parg)])
(weakenNs [tyname, argname] pats)
let clause = MkPatClause {todo = tyname :: argname :: todo}
pvars (newargs ++ pats')
(weakenNs [tyname, argname] rhs)
pure [DelayGroup [clause]]
addDelayG {todo} pty parg pats rhs (g :: gs) with (checkGroupMatch CDelay [] g)
addDelayG {todo} pty parg pats rhs
((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tm) :: rest)) :: gs)
| (DelayMatch {tyarg} {valarg})
= do let newps = newPats [pty, parg] (ConsMatch (ConsMatch NilMatch)) ps
let pats' = updatePatNames (updateNames [(tyarg, pty),
(valarg, parg)])
(weakenNs [tyarg, valarg] pats)
let newclause : PatClause (tyarg :: valarg :: vars)
(tyarg :: valarg :: todo)
= MkPatClause pvars (newps ++ pats')
(weakenNs [tyarg, valarg] rhs)
pure ((DelayGroup (MkPatClause pvars ps tm :: rest ++ [newclause]))
:: gs)
addDelayG pty parg pats rhs (g :: gs) | NoMatch
= do gs' <- addDelayG pty parg pats rhs gs
pure (g :: gs')
addConstG : Constant -> NamedPats vars todo ->
(rhs : Term vars) ->
(acc : List (Group vars todo)) ->
@ -474,6 +528,10 @@ groupCons fc fn pvars cs
= addConG n 0 pargs pats rhs acc
addGroup (PArrow _ _ s t) pprf pats rhs acc
= addConG (UN "->") 0 [s, t] pats rhs acc
-- Go inside the delay; we'll flag the case as needing to force its
-- scrutinee (need to check in 'caseGroups below)
addGroup (PDelay _ _ pty parg) pprf pats rhs acc
= addDelayG pty parg pats rhs acc
addGroup (PConst _ c) pprf pats rhs acc
= addConstG c pats rhs acc
addGroup _ pprf pats rhs acc = pure acc -- Can't happen, not a constructor
@ -552,6 +610,8 @@ samePat (pi :: xs) = samePatAs (getFirstPat pi) (map getFirstPat xs)
else False
samePatAs (PArrow fc x s t) (PArrow _ _ s' t' :: ps)
= samePatAs (PArrow fc x s t) ps
samePatAs (PDelay fc r t p) (PDelay _ _ _ _ :: ps)
= samePatAs (PDelay fc r t p) ps
samePatAs (PLoc fc n) (PLoc _ _ :: ps) = samePatAs (PLoc fc n) ps
samePatAs x y = False
@ -568,6 +628,7 @@ countDiff xs = length (distinct [] (map getFirstCon xs))
isVar (PTyCon _ _ _ _) = False
isVar (PConst _ _) = False
isVar (PArrow _ _ _ _) = False
isVar (PDelay _ _ _ p) = False
isVar _ = True
-- Return whether two patterns would lead to the same match
@ -578,6 +639,7 @@ countDiff xs = length (distinct [] (map getFirstCon xs))
sameCase (PTyCon _ t _ _) (PTyCon _ t' _ _) = t == t'
sameCase (PConst _ c) (PConst _ c') = c == c'
sameCase (PArrow _ _ _ _) (PArrow _ _ _ _) = True
sameCase (PDelay _ _ _ _) (PDelay _ _ _ _) = True
sameCase x y = isVar x && isVar y
distinct : List Pat -> List Pat -> List Pat
@ -672,6 +734,10 @@ mutual
= do crest <- match fc fn phase rest (map (weakenNs newargs) errorCase)
cs' <- altGroups cs
pure (ConCase cn tag newargs crest :: cs')
altGroups (DelayGroup {tyarg} {valarg} rest :: cs)
= do crest <- match fc fn phase rest (map (weakenNs [tyarg, valarg]) errorCase)
cs' <- altGroups cs
pure (DelayCase tyarg valarg crest :: cs')
altGroups (ConstGroup c rest :: cs)
= do crest <- match fc fn phase rest errorCase
cs' <- altGroups cs

17
src/Core/CaseTree.idr
View File

@ -8,7 +8,8 @@ mutual
public export
data CaseTree : List Name -> Type where
Case : {name : _} ->
(idx : Nat) -> IsVar name idx vars ->
(idx : Nat) ->
IsVar name idx vars ->
(scTy : Term vars) -> List (CaseAlt vars) ->
CaseTree vars
STerm : Term vars -> CaseTree vars
@ -19,6 +20,8 @@ mutual
data CaseAlt : List Name -> Type where
ConCase : Name -> (tag : Int) -> (args : List Name) ->
CaseTree (args ++ vars) -> CaseAlt vars
DelayCase : (ty : Name) -> (arg : Name) ->
CaseTree (ty :: arg :: vars) -> CaseAlt vars
ConstCase : Constant -> CaseTree vars -> CaseAlt vars
DefaultCase : CaseTree vars -> CaseAlt vars
@ -30,6 +33,8 @@ data Pat : Type where
PTyCon : FC -> Name -> (arity : Nat) -> List Pat -> Pat
PConst : FC -> (c : Constant) -> Pat
PArrow : FC -> (x : Name) -> Pat -> Pat -> Pat
PDelay : FC -> LazyReason -> Pat -> Pat -> Pat
-- TODO: Matching on lazy types
PLoc : FC -> Name -> Pat
PUnmatchable : FC -> Term [] -> Pat
@ -48,6 +53,8 @@ mutual
show (ConCase n tag args sc)
= show n ++ " " ++ showSep " " (map show args) ++ " => " ++
show sc
show (DelayCase _ arg sc)
= "Delay " ++ show arg ++ " => " ++ show sc
show (ConstCase c sc)
= show c ++ " => " ++ show sc
show (DefaultCase sc)
@ -60,6 +67,7 @@ Show Pat where
show (PTyCon _ n _ args) = "<TyCon>" ++ show n ++ " " ++ assert_total (show args)
show (PConst _ c) = show c
show (PArrow _ x s t) = "(" ++ show s ++ " -> " ++ show t ++ ")"
show (PDelay _ _ _ p) = "(Delay " ++ show p ++ ")"
show (PLoc _ n) = show n
show (PUnmatchable _ tm) = ".(" ++ show tm ++ ")"
@ -83,6 +91,9 @@ mutual
insertCaseNames {outer = args ++ outer} {inner} ns
(rewrite sym (appendAssociative args outer inner) in
ct))
insertCaseAltNames {outer} {inner} ns (DelayCase tyn valn ct)
= DelayCase tyn valn
(insertCaseNames {outer = tyn :: valn :: outer} {inner} ns ct)
insertCaseAltNames ns (ConstCase x ct)
= ConstCase x (insertCaseNames ns ct)
insertCaseAltNames ns (DefaultCase ct)
@ -114,6 +125,8 @@ mkPat' args orig (App fc fn p arg)
mkPat' (parg :: args) orig fn
mkPat' args orig (As fc (Ref _ Bound n) ptm)
= PAs fc n (mkPat' [] ptm ptm)
mkPat' args orig (TDelay fc r ty p)
= PDelay fc r (mkPat' [] orig ty) (mkPat' [] orig p)
mkPat' args orig (PrimVal fc c) = PConst fc c
mkPat' args orig tm = PUnmatchable (getLoc orig) orig
@ -134,6 +147,8 @@ mkTerm vars (PTyCon fc x arity xs)
mkTerm vars (PConst fc c) = PrimVal fc c
mkTerm vars (PArrow fc x s t)
= Bind fc x (Pi RigW Explicit (mkTerm vars s)) (mkTerm (x :: vars) t)
mkTerm vars (PDelay fc r ty p)
= TDelay fc r (mkTerm vars ty) (mkTerm vars p)
mkTerm vars (PLoc fc n)
= case isVar n vars of
Just (MkVar prf) => Local fc Nothing _ prf

68
src/Core/Context.idr
View File

@ -991,8 +991,8 @@ toFullNames tm
= pure (As fc !(full gam p) !(full gam tm))
full gam (TDelayed fc x y)
= pure (TDelayed fc x !(full gam y))
full gam (TDelay fc x y)
= pure (TDelay fc x !(full gam y))
full gam (TDelay fc x t y)
= pure (TDelay fc x !(full gam t) !(full gam y))
full gam (TForce fc y)
= pure (TForce fc !(full gam y))
full gam tm = pure tm
@ -1054,37 +1054,33 @@ checkUnambig fc n
[(fulln, i, _)] => pure (Resolved i)
ns => throw (AmbiguousName fc (map fst ns))
export
setLazy : {auto c : Ref Ctxt Defs} ->
FC -> (delayType : Name) -> (delay : Name) -> (force : Name) ->
(infinite : Name) ->
Core ()
setLazy fc ty d f i
= do defs <- get Ctxt
ty' <- checkUnambig fc ty
d' <- checkUnambig fc d
f' <- checkUnambig fc f
i' <- checkUnambig fc i
put Ctxt (record { options $= setLazy ty' d' f' i' } defs)
export
lazyActive : {auto c : Ref Ctxt Defs} ->
Bool -> Core ()
lazyActive a
= do defs <- get Ctxt
let l = laziness (options defs)
maybe (pure ())
(\lns =>
do let l' = record { active = a } lns
put Ctxt (record { options->laziness = Just l' }
defs)) l
put Ctxt (record { options->elabDirectives->lazyActive = a } defs)
export
autoImplicits : {auto c : Ref Ctxt Defs} ->
Bool -> Core ()
autoImplicits a
= do defs <- get Ctxt
put Ctxt (record { options->elabDirectives->autoImplicits = a } defs)
export
isLazyActive : {auto c : Ref Ctxt Defs} ->
Core Bool
isLazyActive
= do defs <- get Ctxt
pure (maybe False active (laziness (options defs)))
pure (lazyActive (elabDirectives (options defs)))
export
isAutoImplicits : {auto c : Ref Ctxt Defs} ->
Core Bool
isAutoImplicits
= do defs <- get Ctxt
pure (autoImplicits (elabDirectives (options defs)))
export
setPair : {auto c : Ref Ctxt Defs} ->
@ -1130,34 +1126,6 @@ setFromChar n
-- Checking special names from Options
export
isDelayType : Name -> Defs -> Bool
isDelayType n defs
= case laziness (options defs) of
Nothing => False
Just l => active l && n == delayType l
export
isDelay : Name -> Defs -> Bool
isDelay n defs
= case laziness (options defs) of
Nothing => False
Just l => active l && n == delay l
export
isForce : Name -> Defs -> Bool
isForce n defs
= case laziness (options defs) of
Nothing => False
Just l => active l && n == force l
export
isInfinite : Name -> Defs -> Bool
isInfinite n defs
= case laziness (options defs) of
Nothing => False
Just l => active l && n == infinite l
export
isPairType : Name -> Defs -> Bool
isPairType n defs

10
src/Core/GetType.idr
View File

@ -47,17 +47,17 @@ mutual
throw (NotFunctionType fc env fty')
chk env (As fc n p) = chk env p
chk env (TDelayed fc r tm) = pure (gType fc)
chk env (TDelay fc r tm)
= do tm' <- chk env tm
chk env (TDelay fc r dty tm)
= do gtm <- chk env tm
tm' <- getNF gtm
defs <- get Ctxt
let ctm = toClosure defaultOpts env !(getTerm tm')
pure $ glueBack defs env (NDelayed fc r ctm)
pure $ glueBack defs env (NDelayed fc r tm')
chk env (TForce fc tm)
= do tm' <- chk env tm
case !(getNF tm') of
NDelayed fc r fty =>
do defs <- get Ctxt
pure $ glueBack defs env !(evalClosure defs fty)
pure $ glueBack defs env fty
chk env (PrimVal fc x) = pure $ gnf env (chkConstant fc x)
chk env (TType fc) = pure (gType fc)
chk env (Erased fc) = pure (gErased fc)

17
src/Core/Hash.idr
View File

@ -112,8 +112,8 @@ mutual
= h `hashWithSalt` 5 `hashWithSalt` nm `hashWithSalt` pat
hashWithSalt h (TDelayed fc x y)
= h `hashWithSalt` 6 `hashWithSalt` y
hashWithSalt h (TDelay fc x y)
= h `hashWithSalt` 7 `hashWithSalt` y
hashWithSalt h (TDelay fc x t y)
= h `hashWithSalt` 7 `hashWithSalt` t `hashWithSalt` y
hashWithSalt h (TForce fc x)
= h `hashWithSalt` 8 `hashWithSalt` x
hashWithSalt h (PrimVal fc c)
@ -135,10 +135,12 @@ mutual
= h `hashWithSalt` 3 `hashWithSalt` (show c)
hashWithSalt h (PArrow fc x s t)
= h `hashWithSalt` 4 `hashWithSalt` s `hashWithSalt` t
hashWithSalt h (PDelay fc r t p)
= h `hashWithSalt` 5 `hashWithSalt` t `hashWithSalt` p
hashWithSalt h (PLoc fc x)
= h `hashWithSalt` 5 `hashWithSalt` x
hashWithSalt h (PUnmatchable fc x)
= h `hashWithSalt` 6 `hashWithSalt` x
hashWithSalt h (PUnmatchable fc x)
= h `hashWithSalt` 7 `hashWithSalt` x
export
Hashable (CaseTree vars) where
@ -156,9 +158,12 @@ mutual
hashWithSalt h (ConCase x tag args y)
= h `hashWithSalt` 0 `hashWithSalt` x `hashWithSalt` args
`hashWithSalt` y
hashWithSalt h (DelayCase t x y)
= h `hashWithSalt` 2 `hashWithSalt` (show t)
`hashWithSalt` (show x) `hashWithSalt` y
hashWithSalt h (ConstCase x y)
= h `hashWithSalt` 1 `hashWithSalt` (show x) `hashWithSalt` y
= h `hashWithSalt` 3 `hashWithSalt` (show x) `hashWithSalt` y
hashWithSalt h (DefaultCase x)
= h `hashWithSalt` 2 `hashWithSalt` x
= h `hashWithSalt` 4 `hashWithSalt` x

12
src/Core/LinearCheck.idr
View File

@ -151,7 +151,7 @@ mutual
pure (h || h')
updateHoleUsage useInHole var (TDelayed _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TDelay _ _ t)
updateHoleUsage useInHole var (TDelay _ _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TForce _ t)
= updateHoleUsage useInHole var t
@ -305,17 +305,17 @@ mutual
lcheck rig erase env (TDelayed fc r ty)
= do (ty', _, u) <- lcheck rig erase env ty
pure (TDelayed fc r ty', gType fc, u)
lcheck rig erase env (TDelay fc r val)
= do (val', gty, u) <- lcheck rig erase env val
lcheck rig erase env (TDelay fc r ty val)
= do (ty', _, _) <- lcheck Rig0 erase env ty
(val', gty, u) <- lcheck rig erase env val
ty <- getTerm gty
pure (TDelay fc r val', gnf env (TDelayed fc r ty), u)
pure (TDelay fc r ty' val', gnf env (TDelayed fc r ty), u)
lcheck rig erase env (TForce fc val)
= do (val', gty, u) <- lcheck rig erase env val
tynf <- getNF gty
case tynf of
NDelayed _ r arg
NDelayed _ r narg
=> do defs <- get Ctxt
narg <- evalClosure defs arg
pure (TForce fc val', glueBack defs env narg, u)
_ => throw (GenericMsg fc "Not a delayed tyoe")
lcheck rig erase env (PrimVal fc c)

41
src/Core/Normalise.idr
View File

@ -99,13 +99,15 @@ parameters (defs : Defs, topopts : EvalOpts)
tm' <- eval env locs tm stk
pure (NAs fc n' tm')
eval env locs (TDelayed fc r ty) stk
= pure (NDelayed fc r (MkClosure topopts locs env ty))
eval env locs (TDelay fc r tm) stk
= pure (NDelay fc r (MkClosure topopts locs env tm))
= do ty' <- eval env locs ty stk
pure (NDelayed fc r ty')
eval env locs (TDelay fc r ty tm) stk
= pure (NDelay fc r (MkClosure topopts locs env ty)
(MkClosure topopts locs env tm))
eval env locs (TForce fc tm) stk
= do tm' <- eval env locs tm stk
case tm' of
NDelay fc r arg => evalClosure defs arg
NDelay fc r _ arg => evalClosure defs arg
_ => pure (NForce fc tm')
eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c
eval env locs (Erased fc) stk = pure $ NErased fc
@ -240,6 +242,9 @@ parameters (defs : Defs, topopts : EvalOpts)
[(explApp Nothing, MkNFClosure aty),
(explApp Nothing, MkNFClosure (NBind pfc x (Lam r e aty) scty))]
sc def
-- Delay matching
tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc) def
= evalTree env (ty :: arg :: loc) opts fc stk sc def
-- Constant matching
tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc) def
= if c == c' then evalTree env loc opts fc stk sc def
@ -513,16 +518,28 @@ mutual
pat' <- quoteGenNF q defs bound env pat
pure (As fc n' pat')
quoteGenNF q defs bound env (NDelayed fc r arg)
= do argNF <- evalClosure defs arg
argQ <- quoteGenNF q defs bound env argNF
= do argQ <- quoteGenNF q defs bound env arg
pure (TDelayed fc r argQ)
quoteGenNF q defs bound env (NDelay fc r arg)
quoteGenNF q defs bound env (NDelay fc LInf ty arg)
= do argNF <- evalClosure defs (toHolesOnly arg)
argQ <- quoteGenNF q defs bound env argNF
tyNF <- evalClosure defs (toHolesOnly ty)
tyQ <- quoteGenNF q defs bound env tyNF
pure (TDelay fc LInf tyQ argQ)
where
toHolesOnly : Closure vs -> Closure vs
toHolesOnly (MkClosure _ locs env tm)
= MkClosure withArgHoles locs env tm
toHolesOnly c = c
quoteGenNF q defs bound env (NDelay fc r ty arg)
= do argNF <- evalClosure defs arg
argQ <- quoteGenNF q defs bound env argNF
pure (TDelay fc r argQ)
tyNF <- evalClosure defs ty
tyQ <- quoteGenNF q defs bound env tyNF
pure (TDelay fc r tyQ argQ)
quoteGenNF q defs bound env (NForce fc arg)
= case arg of
NDelay fc _ arg =>
NDelay fc _ _ arg =>
do argNF <- evalClosure defs arg
quoteGenNF q defs bound env argNF
t => do arg' <- quoteGenNF q defs bound env arg
@ -674,11 +691,11 @@ mutual
= convGen q defs env tm tm'
convGen q defs env (NDelayed _ r arg) (NDelayed _ r' arg')
= if r == r'
= if compatible r r'
then convGen q defs env arg arg'
else pure False
convGen q defs env (NDelay _ r arg) (NDelay _ r' arg')
= if r == r'
convGen q defs env (NDelay _ r _ arg) (NDelay _ r' _ arg')
= if compatible r r'
then convGen q defs env arg arg'
else pure False
convGen q defs env (NForce _ arg) (NForce _ arg')

41
src/Core/Options.idr
View File

@ -57,15 +57,6 @@ getCG : String -> Maybe CG
getCG cg = lookup (toLower cg) availableCGs
-- Name options, to be saved in TTC
public export
record LazyNames where
constructor MkLazy
active : Bool
delayType : Name
delay : Name
force : Name
infinite : Name
public export
record PairNames where
constructor MkPairNs
@ -86,20 +77,6 @@ record PrimNames where
fromStringName : Maybe Name
fromCharName : Maybe Name
export
TTC LazyNames where
toBuf b l
= do toBuf b (delayType l)
toBuf b (delay l)
toBuf b (force l)
toBuf b (infinite l)
fromBuf r b
= do ty <- fromBuf r b
d <- fromBuf r b
f <- fromBuf r b
i <- fromBuf r b
pure (MkLazy True ty d f i)
export
TTC PairNames where
toBuf b l
@ -135,6 +112,12 @@ TTC PrimNames where
pure (MkPrimNs i str c)
-- Other options relevant to the current session (so not to be saved in a TTC)
public export
record ElabDirectives where
constructor MkElabDirectives
lazyActive : Bool
autoImplicits : Bool
public export
record Session where
constructor MkSessionOpts
@ -156,7 +139,7 @@ record Options where
dirs : Dirs
printing : PPrinter
session : Session
laziness : Maybe LazyNames
elabDirectives : ElabDirectives
pairnames : Maybe PairNames
rewritenames : Maybe RewriteNames
primnames : PrimNames
@ -171,18 +154,16 @@ defaultPPrint = MkPPOpts False True False
defaultSession : Session
defaultSession = MkSessionOpts False Chez 0 False
defaultElab : ElabDirectives
defaultElab = MkElabDirectives True True
export
defaults : Options
defaults = MkOptions defaultDirs defaultPPrint defaultSession
Nothing Nothing Nothing
defaultElab Nothing Nothing
(MkPrimNs Nothing Nothing Nothing)
[]
export
setLazy : (delayType : Name) -> (delay : Name) -> (force : Name) ->
(infinite : Name) -> Options -> Options
setLazy ty d f i = record { laziness = Just (MkLazy True ty d f i) }
export
setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
Options -> Options

54
src/Core/TT.idr
View File

@ -350,7 +350,7 @@ namespace CList
-- These are guaranteed to be well-scoped wrt local variables, because they are
-- indexed by the names of local variables in scope
public export
data LazyReason = LInf | LLazy
data LazyReason = LInf | LLazy | LUnknown
public export
data Term : List Name -> Type where
@ -374,7 +374,7 @@ data Term : List Name -> Type where
As : FC -> (as : Term vars) -> (pat : Term vars) -> Term vars
-- Typed laziness annotations
TDelayed : FC -> LazyReason -> Term vars -> Term vars
TDelay : FC -> LazyReason -> Term vars -> Term vars
TDelay : FC -> LazyReason -> (ty : Term vars) -> (arg : Term vars) -> Term vars
TForce : FC -> Term vars -> Term vars
PrimVal : FC -> (c : Constant) -> Term vars
Erased : FC -> Term vars
@ -389,7 +389,7 @@ getLoc (Bind fc x b scope) = fc
getLoc (App fc fn p arg) = fc
getLoc (As fc x y) = fc
getLoc (TDelayed fc x y) = fc
getLoc (TDelay fc x y) = fc
getLoc (TDelay fc x t y) = fc
getLoc (TForce fc x) = fc
getLoc (PrimVal fc c) = fc
getLoc (Erased fc) = fc
@ -399,8 +399,15 @@ export
Eq LazyReason where
(==) LInf LInf = True
(==) LLazy LLazy = True
(==) LUnknown LUnknown = True
(==) _ _ = False
export
compatible : LazyReason -> LazyReason -> Bool
compatible LUnknown _ = True
compatible _ LUnknown = True
compatible x y = x == y
export
Eq a => Eq (Binder a) where
(Lam c p ty) == (Lam c' p' ty') = c == c' && p == p' && ty == ty'
@ -422,7 +429,7 @@ Eq (Term vars) where
(==) (App _ f _ a) (App _ f' _ a') = f == f' && a == a'
(==) (As _ a p) (As _ a' p') = a == a' && p == p'
(==) (TDelayed _ _ t) (TDelayed _ _ t') = t == t'
(==) (TDelay _ _ t) (TDelay _ _ t') = t == t'
(==) (TDelay _ _ t x) (TDelay _ _ t' x') = t == t' && x == x'
(==) (TForce _ t) (TForce _ t') = t == t'
(==) (PrimVal _ c) (PrimVal _ c') = c == c'
(==) (Erased _) (Erased _) = True
@ -589,7 +596,7 @@ thin {outer} {inner} n (Bind fc x b scope)
thin n (App fc fn p arg) = App fc (thin n fn) p (thin n arg)
thin n (As fc nm tm) = As fc (thin n nm) (thin n tm)
thin n (TDelayed fc r ty) = TDelayed fc r (thin n ty)
thin n (TDelay fc r tm) = TDelay fc r (thin n tm)
thin n (TDelay fc r ty tm) = TDelay fc r (thin n ty) (thin n tm)
thin n (TForce fc tm) = TForce fc (thin n tm)
thin n (PrimVal fc c) = PrimVal fc c
thin n (Erased fc) = Erased fc
@ -613,7 +620,8 @@ insertNames ns (App fc fn p arg)
insertNames ns (As fc as tm)
= As fc (insertNames ns as) (insertNames ns tm)
insertNames ns (TDelayed fc r ty) = TDelayed fc r (insertNames ns ty)
insertNames ns (TDelay fc r tm) = TDelay fc r (insertNames ns tm)
insertNames ns (TDelay fc r ty tm)
= TDelay fc r (insertNames ns ty) (insertNames ns tm)
insertNames ns (TForce fc tm) = TForce fc (insertNames ns tm)
insertNames ns (PrimVal fc c) = PrimVal fc c
insertNames ns (Erased fc) = Erased fc
@ -727,7 +735,8 @@ renameVars prf (App fc fn p arg)
renameVars prf (As fc as tm)
= As fc (renameVars prf as) (renameVars prf tm)
renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
renameVars prf (TDelay fc r tm) = TDelay fc r (renameVars prf tm)
renameVars prf (TDelay fc r ty tm)
= TDelay fc r (renameVars prf ty) (renameVars prf tm)
renameVars prf (TForce fc x) = TForce fc (renameVars prf x)
renameVars prf (PrimVal fc c) = PrimVal fc c
renameVars prf (Erased fc) = Erased fc
@ -799,8 +808,8 @@ mutual
= Just (As fc !(shrinkTerm as prf) !(shrinkTerm tm prf))
shrinkTerm (TDelayed fc x y) prf
= Just (TDelayed fc x !(shrinkTerm y prf))
shrinkTerm (TDelay fc x y) prf
= Just (TDelay fc x !(shrinkTerm y prf))
shrinkTerm (TDelay fc x t y) prf
= Just (TDelay fc x !(shrinkTerm t prf) !(shrinkTerm y prf))
shrinkTerm (TForce fc x) prf
= Just (TForce fc !(shrinkTerm x prf))
shrinkTerm (PrimVal fc c) prf = Just (PrimVal fc c)
@ -856,8 +865,8 @@ mkLocals bs (As fc as tm)
= As fc (mkLocals bs as) (mkLocals bs tm)
mkLocals bs (TDelayed fc x y)
= TDelayed fc x (mkLocals bs y)
mkLocals bs (TDelay fc x y)
= TDelay fc x (mkLocals bs y)
mkLocals bs (TDelay fc x t y)
= TDelay fc x (mkLocals bs t) (mkLocals bs y)
mkLocals bs (TForce fc x)
= TForce fc (mkLocals bs x)
mkLocals bs (PrimVal fc c) = PrimVal fc c
@ -894,8 +903,8 @@ resolveNames vars (As fc as pat)
= As fc (resolveNames vars as) (resolveNames vars pat)
resolveNames vars (TDelayed fc x y)
= TDelayed fc x (resolveNames vars y)
resolveNames vars (TDelay fc x y)
= TDelay fc x (resolveNames vars y)
resolveNames vars (TDelay fc x t y)
= TDelay fc x (resolveNames vars t) (resolveNames vars y)
resolveNames vars (TForce fc x)
= TForce fc (resolveNames vars x)
resolveNames vars tm = tm
@ -944,7 +953,8 @@ namespace SubstEnv
substEnv env (As fc as pat)
= As fc (substEnv env as) (substEnv env pat)
substEnv env (TDelayed fc x y) = TDelayed fc x (substEnv env y)
substEnv env (TDelay fc x y) = TDelay fc x (substEnv env y)
substEnv env (TDelay fc x t y)
= TDelay fc x (substEnv env t) (substEnv env y)
substEnv env (TForce fc x) = TForce fc (substEnv env x)
substEnv env (PrimVal fc c) = PrimVal fc c
substEnv env (Erased fc) = Erased fc
@ -977,8 +987,8 @@ substName x new (As fc as pat)
= As fc (substName x new as) (substName x new pat)
substName x new (TDelayed fc y z)
= TDelayed fc y (substName x new z)
substName x new (TDelay fc y z)
= TDelay fc y (substName x new z)
substName x new (TDelay fc y t z)
= TDelay fc y (substName x new t) (substName x new z)
substName x new (TForce fc y)
= TForce fc (substName x new y)
substName x new tm = tm
@ -996,7 +1006,8 @@ addMetas ns (App fc fn p arg)
= addMetas (addMetas ns fn) arg
addMetas ns (As fc as tm) = addMetas ns tm
addMetas ns (TDelayed fc x y) = addMetas ns y
addMetas ns (TDelay fc x y) = addMetas ns y
addMetas ns (TDelay fc x t y)
= addMetas (addMetas ns t) y
addMetas ns (TForce fc x) = addMetas ns x
addMetas ns (PrimVal fc c) = ns
addMetas ns (Erased fc) = ns
@ -1020,7 +1031,8 @@ addRefs ns (App fc fn p arg)
= addRefs (addRefs ns fn) arg
addRefs ns (As fc as tm) = addRefs ns tm
addRefs ns (TDelayed fc x y) = addRefs ns y
addRefs ns (TDelay fc x y) = addRefs ns y
addRefs ns (TDelay fc x t y)
= addRefs (addRefs ns t) y
addRefs ns (TForce fc x) = addRefs ns x
addRefs ns (PrimVal fc c) = ns
addRefs ns (Erased fc) = ns
@ -1066,9 +1078,9 @@ export Show (Term vars) where
" => " ++ show sc
showApp (App _ _ _ _) [] = "[can't happen]"
showApp (As _ n tm) [] = show n ++ "@" ++ show tm
showApp (TDelayed _ _ tm) [] = "Delayed " ++ show tm
showApp (TDelay _ _ tm) [] = "Delay " ++ show tm
showApp (TForce _ tm) [] = "Force " ++ show tm
showApp (TDelayed _ _ tm) [] = "%Delayed " ++ show tm
showApp (TDelay _ _ _ tm) [] = "%Delay " ++ show tm
showApp (TForce _ tm) [] = "%Force " ++ show tm
showApp (PrimVal _ c) [] = show c
showApp (Erased _) [] = "[__]"
showApp (TType _) [] = "Type"

36
src/Core/TTC.idr
View File

@ -123,11 +123,13 @@ export
TTC LazyReason where
toBuf b LInf = tag 0
toBuf b LLazy = tag 1
toBuf b LUnknown = tag 2
fromBuf r b
= case !getTag of
0 => pure LInf
1 => pure LLazy
2 => pure LUnknown
_ => corrupt "LazyReason"
export
@ -222,9 +224,9 @@ mutual
toBuf b (TDelayed fc r tm)
= do tag 6;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TDelay fc r tm)
toBuf b (TDelay fc r ty tm)
= do tag 7;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b fc; toBuf b r; toBuf b ty; toBuf b tm
toBuf b (TForce fc tm)
= do tag 8;
toBuf b fc; toBuf b tm
@ -265,8 +267,9 @@ mutual
pure (As fc as tm)
6 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
pure (TDelayed fc lr tm)
7 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
pure (TDelay fc lr tm)
7 => do fc <- fromBuf r b; lr <- fromBuf r b;
ty <- fromBuf r b; tm <- fromBuf r b
pure (TDelay fc lr ty tm)
8 => do fc <- fromBuf r b; tm <- fromBuf r b
pure (TForce fc tm)
9 => do fc <- fromBuf r b; c <- fromBuf r b
@ -290,10 +293,12 @@ TTC Pat where
= do tag 3; toBuf b fc; toBuf b c
toBuf b (PArrow fc x s t)
= do tag 4; toBuf b fc; toBuf b x; toBuf b s; toBuf b t
toBuf b (PDelay fc x t y)
= do tag 5; toBuf b fc; toBuf b x; toBuf b t; toBuf b y
toBuf b (PLoc fc x)
= do tag 5; toBuf b fc; toBuf b x
toBuf b (PUnmatchable fc x)
= do tag 6; toBuf b fc; toBuf b x
toBuf b (PUnmatchable fc x)
= do tag 7; toBuf b fc; toBuf b x
fromBuf r b
= case !getTag of
@ -313,9 +318,12 @@ TTC Pat where
4 => do fc <- fromBuf r b; x <- fromBuf r b
s <- fromBuf r b; t <- fromBuf r b
pure (PArrow fc x s t)
5 => do fc <- fromBuf r b; x <- fromBuf r b
pure (PLoc fc x)
5 => do fc <- fromBuf r b; x <- fromBuf r b;
t <- fromBuf r b; y <- fromBuf r b
pure (PDelay fc x t y)
6 => do fc <- fromBuf r b; x <- fromBuf r b
pure (PLoc fc x)
7 => do fc <- fromBuf r b; x <- fromBuf r b
pure (PUnmatchable fc x)
_ => corrupt "Pat"
@ -346,19 +354,23 @@ mutual
TTC (CaseAlt vars) where
toBuf b (ConCase x t args y)
= do tag 0; toBuf b x; toBuf b t; toBuf b args; toBuf b y
toBuf b (DelayCase ty arg y)
= do tag 1; toBuf b ty; toBuf b arg; toBuf b y
toBuf b (ConstCase x y)
= do tag 1; toBuf b x; toBuf b y
= do tag 2; toBuf b x; toBuf b y
toBuf b (DefaultCase x)
= do tag 2; toBuf b x
= do tag 3; toBuf b x
fromBuf r b
= case !getTag of
0 => do x <- fromBuf r b; t <- fromBuf r b
args <- fromBuf r b; y <- fromBuf r b
pure (ConCase x t args y)
1 => do x <- fromBuf r b; y <- fromBuf r b
1 => do ty <- fromBuf r b; arg <- fromBuf r b; y <- fromBuf r b
pure (DelayCase ty arg y)
2 => do x <- fromBuf r b; y <- fromBuf r b
pure (ConstCase x y)
2 => do x <- fromBuf r b
3 => do x <- fromBuf r b
pure (DefaultCase x)
_ => corrupt "CaseAlt"

62
src/Core/Unify.idr
View File

@ -28,29 +28,37 @@ Eq UnifyMode where
InSearch == InSearch = True
_ == _ = False
-- If we're unifying a Lazy type with a non-lazy type, we need to add an
-- explicit force or delay to the first argument to unification. This says
-- which to add, if any. Can only added at the very top level.
public export
data AddLazy = NoLazy | AddForce | AddDelay LazyReason
public export
record UnifyResult where
constructor MkUnifyResult
constraints : List Int
holesSolved : Bool
addLazy : AddLazy
union : UnifyResult -> UnifyResult -> UnifyResult
union u1 u2 = MkUnifyResult (union (constraints u1) (constraints u2))
(holesSolved u1 || holesSolved u2)
NoLazy -- only top level, so assume no annotation
unionAll : List UnifyResult -> UnifyResult
unionAll [] = MkUnifyResult [] False
unionAll [] = MkUnifyResult [] False NoLazy
unionAll [c] = c
unionAll (c :: cs) = union c (unionAll cs)
constrain : Int -> UnifyResult
constrain c = MkUnifyResult [c] False
constrain c = MkUnifyResult [c] False NoLazy
success : UnifyResult
success = MkUnifyResult [] False
success = MkUnifyResult [] False NoLazy
solvedHole : UnifyResult
solvedHole = MkUnifyResult [] True
solvedHole = MkUnifyResult [] True NoLazy
public export
interface Unify (tm : List Name -> Type) where
@ -61,6 +69,15 @@ interface Unify (tm : List Name -> Type) where
FC -> Env Term vars ->
tm vars -> tm vars ->
Core UnifyResult
-- As unify but at the top level can allow lazy/non-lazy to be mixed in
-- order to infer annotations
unifyWithLazyD : Ref Ctxt Defs ->
Ref UST UState ->
UnifyMode ->
FC -> Env Term vars ->
tm vars -> tm vars ->
Core UnifyResult
unifyWithLazyD = unifyD
-- Workaround for auto implicits not working in interfaces
-- In calls to unification, the first argument is the given type, and the second
@ -75,6 +92,16 @@ unify : Unify tm =>
Core UnifyResult
unify {c} {u} = unifyD c u
export
unifyWithLazy : Unify tm =>
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
UnifyMode ->
FC -> Env Term vars ->
tm vars -> tm vars ->
Core UnifyResult
unifyWithLazy {c} {u} = unifyWithLazyD c u
-- Defined in Core.AutoSearch
export
search : {auto c : Ref Ctxt Defs} ->
@ -656,7 +683,12 @@ mutual
else convertError loc env
(NTCon xfc x tagx ax xs)
(NTCon yfc y tagy ay ys)
unifyNoEta mode loc env (NDelayed xfc _ x) (NDelayed yfc _ y)
= unify mode loc env x y
unifyNoEta mode loc env (NDelay xfc _ xty x) (NDelay yfc _ yty y)
= unifyArgs mode loc env [xty, x] [yty, y]
unifyNoEta mode loc env (NForce xfc x) (NForce yfc y)
= unify mode loc env x y
unifyNoEta mode loc env (NApp xfc fx axs) (NApp yfc fy ays)
= unifyBothApps mode loc env xfc fx axs yfc fy ays
unifyNoEta mode loc env (NApp xfc hd args) y
@ -740,15 +772,33 @@ mutual
_ => unifyNoEta mode loc env tmx tmy
unifyD _ _ mode loc env tmx tmy = unifyNoEta mode loc env tmx tmy
unifyWithLazyD _ _ mode loc env (NDelayed _ _ tmx) (NDelayed _ _ tmy)
= unify mode loc env tmx tmy
unifyWithLazyD _ _ mode loc env (NDelayed _ r tmx) tmy
= do vs <- unify mode loc env tmx tmy
pure (record { addLazy = AddForce } vs)
unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy)
= do vs <- unify mode loc env tmx tmy
pure (record { addLazy = AddDelay r } vs)
unifyWithLazyD _ _ mode loc env tmx tmy
= unify mode loc env tmx tmy
export
Unify Term where
unifyD _ _ mode loc env x y
= do defs <- get Ctxt
if x == y
then do log 10 $ "Skipped unification (equal already): "
then do log 10 $ "S§kipped unification (equal already): "
++ show x ++ " and " ++ show y
pure success
else unify mode loc env !(nf defs env x) !(nf defs env y)
unifyWithLazyD _ _ mode loc env x y
= do defs <- get Ctxt
if x == y
then do log 10 $ "Skipped unification (equal already): "
++ show x ++ " and " ++ show y
pure success
else unifyWithLazy mode loc env !(nf defs env x) !(nf defs env y)
export
Unify Closure where

4
src/Core/Value.idr
View File

@ -68,8 +68,8 @@ mutual
NTCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
List (AppInfo, Closure vars) -> NF vars
NAs : FC -> NF vars -> NF vars -> NF vars
NDelayed : FC -> LazyReason -> Closure vars -> NF vars
NDelay : FC -> LazyReason -> Closure vars -> NF vars
NDelayed : FC -> LazyReason -> NF vars -> NF vars
NDelay : FC -> LazyReason -> Closure vars -> Closure vars -> NF vars
NForce : FC -> NF vars -> NF vars
NPrimVal : FC -> Constant -> NF vars
NErased : FC -> NF vars

3
src/Parser/Lexer.idr
View File

@ -102,7 +102,8 @@ keywords = ["data", "module", "where", "let", "in", "do", "record",
"public", "export", "private",
"infixl", "infixr", "infix", "prefix",
"Type", "Int", "Integer", "String", "Char", "Double",
"total", "partial", "covering"]
"total", "partial", "covering",
"Lazy", "Inf", "Delay", "Force"]
-- Reserved words for internal syntax
special : List String

8
src/TTImp/Elab/Ambiguity.idr
View File

@ -100,16 +100,16 @@ expandAmbigName mode env orig args (IImplicitApp fc f n a) exp
((fc, Just n, a) :: args) f exp
expandAmbigName elabmode env orig args tm exp = pure orig
stripDelay : Defs -> NF vars -> Core (NF vars)
stripDelay defs (NDelayed fc r t) = evalClosure defs t
stripDelay defs tm = pure tm
stripDelay : Defs -> NF vars -> NF vars
stripDelay defs (NDelayed fc r t) = t
stripDelay defs tm = tm
data TypeMatch = Concrete | Poly | NoMatch
mutual
mightMatchD : Defs -> NF vars -> NF [] -> Core TypeMatch
mightMatchD defs l r
= mightMatch defs !(stripDelay defs l) !(stripDelay defs r)
= mightMatch defs (stripDelay defs l) (stripDelay defs r)
mightMatchArg : Defs ->
(AppInfo, Closure vars) -> (AppInfo, Closure []) ->

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

@ -211,8 +211,9 @@ mutual
-- better way that leads to good code...)
ok <- solveIfUndefined env metaval argv
when (not ok) $
do [] <- convert fc elabinfo env (gnf env metaval)
do res <- convert fc elabinfo env (gnf env metaval)
(gnf env argv)
let [] = constraints res
| cs => throw (CantConvert fc env metaval argv)
pure ()
case elabMode elabinfo of
@ -350,7 +351,8 @@ mutual
logGlue 10 "Expected function type" env expfnty
maybe (pure ()) (logGlue 10 "Expected result type" env) expty
res <- checkAppWith rig elabinfo nest env fc fntm fnty expargs impargs kr expty
[] <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty
cres <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty
let [] = constraints cres
| cs => do cty <- getTerm expfnty
ctm <- newConstant fc rig env (fst res) cty cs
pure (ctm, expfnty)

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

@ -46,7 +46,7 @@ mutual
findUsed env used (As _ as pat)
= findUsed env (findUsed env used as) pat
findUsed env used (TDelayed _ _ tm) = findUsed env used tm
findUsed env used (TDelay _ _ tm) = findUsed env used tm
findUsed env used (TDelay _ _ _ tm) = findUsed env used tm
findUsed env used (TForce _ tm) = findUsed env used tm
findUsed env used _ = used
@ -87,8 +87,8 @@ changeVar old new (As fc nm p)
= As fc (changeVar old new nm) (changeVar old new p)
changeVar old new (TDelayed fc r p)
= TDelayed fc r (changeVar old new p)
changeVar old new (TDelay fc r p)
= TDelay fc r (changeVar old new p)
changeVar old new (TDelay fc r t p)
= TDelay fc r (changeVar old new t) (changeVar old new p)
changeVar old new (TForce fc p)
= TForce fc (changeVar old new p)
changeVar old new tm = tm

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

@ -454,7 +454,7 @@ convert : {vars : _} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
Core (List Int)
Core UnifyResult
convert fc elabinfo env x y
= let umode : UnifyMode
= case elabMode elabinfo of
@ -463,13 +463,13 @@ convert fc elabinfo env x y
catch (do vs <- if isFromTerm x && isFromTerm y
then do xtm <- getTerm x
ytm <- getTerm y
unify umode fc env xtm ytm
unifyWithLazy umode fc env xtm ytm
else do xnf <- getNF x
ynf <- getNF y
unify umode fc env xnf ynf
unifyWithLazy umode fc env xnf ynf
when (holesSolved vs) $
solveConstraints umode Normal
pure (constraints vs))
pure vs)
(\err => do xtm <- getTerm x
ytm <- getTerm y
-- See if we can improve the error message by
@ -493,9 +493,13 @@ checkExp : {vars : _} ->
(got : Glued vars) -> (expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkExp rig elabinfo env fc tm got (Just exp)
= do constr <- convert fc elabinfo env got exp
case constr of
[] => pure (tm, got)
= do vs <- convert fc elabinfo env got exp
case (constraints vs) of
[] => case addLazy vs of
NoLazy => pure (tm, got)
AddForce => pure (TForce fc tm, exp)
AddDelay r => do ty <- getTerm got
pure (TDelay fc r ty tm, exp)
cs => do defs <- get Ctxt
empty <- clearDefs defs
cty <- getTerm exp

2
src/TTImp/Elab/Hole.idr
View File

@ -1,4 +1,4 @@
module TTImp.Elab.As
module TTImp.Elab.Hole
import Core.Context
import Core.Core

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

@ -43,7 +43,8 @@ mutual
embedSub sub (As fc nm pat)
= As fc (embedSub sub nm) (embedSub sub pat)
embedSub sub (TDelayed fc x y) = TDelayed fc x (embedSub sub y)
embedSub sub (TDelay fc x y) = TDelay fc x (embedSub sub y)
embedSub sub (TDelay fc x t y)
= TDelay fc x (embedSub sub t) (embedSub sub y)
embedSub sub (TForce fc x) = TForce fc (embedSub sub x)
embedSub sub (PrimVal fc c) = PrimVal fc c
embedSub sub (Erased fc) = Erased fc
@ -199,7 +200,7 @@ swapVars {vs} (Bind fc x b scope)
swapVars (App fc fn p arg) = App fc (swapVars fn) p (swapVars arg)
swapVars (As fc nm pat) = As fc (swapVars nm) (swapVars pat)
swapVars (TDelayed fc x tm) = TDelayed fc x (swapVars tm)
swapVars (TDelay fc x tm) = TDelay fc x (swapVars tm)
swapVars (TDelay fc x ty tm) = TDelay fc x (swapVars ty) (swapVars tm)
swapVars (TForce fc tm) = TForce fc (swapVars tm)
swapVars (PrimVal fc c) = PrimVal fc c
swapVars (Erased fc) = Erased fc

88
src/TTImp/Elab/Lazy.idr Normal file
View File

@ -0,0 +1,88 @@
module TTImp.Elab.Lazy
import Core.Context
import Core.Core
import Core.Env
import Core.Normalise
import Core.Unify
import Core.TT
import Core.Value
import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp
%default covering
export
checkDelayed : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> LazyReason -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkDelayed rig elabinfo nest env fc r tm exp
= do (tm', gty) <- check rig elabinfo nest env tm (Just (gType fc))
pure (TDelayed fc r tm', gty)
export
checkDelay : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkDelay rig elabinfo nest env fc tm mexpected
= do expected <- maybe (do nm <- genName "delayTy"
ty <- metaVar fc Rig0 env nm (TType fc)
pure (gnf env ty))
pure mexpected
let solvemode = case elabMode elabinfo of
InLHS c => InLHS
_ => InTerm
solveConstraints solvemode Normal
-- Can only check if we know the expected type already because we
-- need to infer the delay reason
delayOnFailure fc rig env expected delayError
(\delayed =>
case !(getNF expected) of
NDelayed _ r expnf =>
do defs <- get Ctxt
(tm', gty) <- check rig elabinfo nest env tm
(Just (glueBack defs env expnf))
tynf <- getNF gty
ty <- getTerm gty
pure (TDelay fc r ty tm',
glueBack defs env (NDelayed fc r tynf))
_ => throw (GenericMsg fc ("Can't infer delay type")))
where
delayError : Error -> Bool
delayError (GenericMsg _ _) = True
delayError _ = False
export
checkForce : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkForce rig elabinfo nest env fc tm exp
= do defs <- get Ctxt
expf <- maybe (pure Nothing)
(\gty => do tynf <- getNF gty
pure (Just (glueBack defs env
(NDelayed fc LUnknown tynf))))
exp
(tm', gty) <- check rig elabinfo nest env tm expf
tynf <- getNF gty
case tynf of
NDelayed _ _ expnf =>
pure (TForce fc tm', glueBack defs env expnf)
_ => throw (GenericMsg fc "Forcing a non-delayed type")

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

@ -16,6 +16,7 @@ import TTImp.Elab.Case
import TTImp.Elab.Check
import TTImp.Elab.Hole
import TTImp.Elab.ImplicitBind
import TTImp.Elab.Lazy
import TTImp.Elab.Local
import TTImp.Elab.Prim
import TTImp.TTImp
@ -135,7 +136,12 @@ checkTerm rig elabinfo nest env (IAs fc side n_in tm) exp
= checkAs rig elabinfo nest env fc side n_in tm exp
checkTerm rig elabinfo nest env (IMustUnify fc n tm) exp
= throw (InternalError ("Dot patterns not implemented: " ++ n ++ " " ++ show tm))
checkTerm rig elabinfo nest env (IDelayed fc r tm) exp
= checkDelayed rig elabinfo nest env fc r tm exp
checkTerm rig elabinfo nest env (IDelay fc tm) exp
= checkDelay rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IForce fc tm) exp
= checkForce rig elabinfo nest env fc tm exp
checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp
= do let (cval, cty) = checkPrim {vars} fc c
checkExp rig elabinfo env fc cval (gnf env cty) exp

25
src/TTImp/Parser.idr
View File

@ -72,6 +72,7 @@ mutual
appExpr : FileName -> IndentInfo -> Rule RawImp
appExpr fname indents
= case_ fname indents
<|> lazy fname indents
<|> do start <- location
f <- simpleExpr fname indents
args <- many (argExpr fname indents)
@ -308,6 +309,30 @@ mutual
end <- location
pure (ImpossibleClause (MkFC fname start end) lhs)
lazy : FileName -> IndentInfo -> Rule RawImp
lazy fname indents
= do start <- location
keyword "Lazy"
tm <- simpleExpr fname indents
end <- location
pure (IDelayed (MkFC fname start end) LLazy tm)
<|> do start <- location
keyword "Inf"
tm <- simpleExpr fname indents
end <- location
pure (IDelayed (MkFC fname start end) LInf tm)
<|> do start <- location
keyword "Delay"
tm <- simpleExpr fname indents
end <- location
pure (IDelay (MkFC fname start end) tm)
<|> do start <- location
keyword "Force"
tm <- simpleExpr fname indents
end <- location
pure (IForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> Rule RawImp
binder fname indents
= autoImplicitPi fname indents

11
src/TTImp/TTImp.idr
View File

@ -71,6 +71,11 @@ mutual
-- by unification
IMustUnify : FC -> (reason : String) -> RawImp -> RawImp
-- Laziness annotations
IDelayed : FC -> LazyReason -> RawImp -> RawImp -- the type
IDelay : FC -> RawImp -> RawImp -- delay constructor
IForce : FC -> RawImp -> RawImp
IPrimVal : FC -> (c : Constant) -> RawImp
IType : FC -> RawImp
IHole : FC -> String -> RawImp
@ -127,6 +132,9 @@ mutual
show (IBindVar fc n) = "$" ++ n
show (IAs fc _ n tm) = show n ++ "@(" ++ show tm ++ ")"
show (IMustUnify fc r tm) = ".(" ++ show tm ++ ")"
show (IDelayed fc r tm) = "(%delayed " ++ show tm ++ ")"
show (IDelay fc tm) = "(%delay " ++ show tm ++ ")"
show (IForce fc tm) = "(%force " ++ show tm ++ ")"
show (IPrimVal fc c) = show c
show (IHole _ x) = "?" ++ x
show (IType fc) = "%type"
@ -269,6 +277,9 @@ getFC (IType x) = x
getFC (IBindVar x _) = x
getFC (IBindHere x _ _) = x
getFC (IMustUnify x _ _) = x
getFC (IDelayed x _ _) = x
getFC (IDelay x _) = x
getFC (IForce x _) = x
getFC (IAs x _ _ _) = x
getFC (Implicit x _) = x

28
src/TTImp/Unelab.idr
View File

@ -22,7 +22,7 @@ used idx (Meta _ _ _ args) = any (used idx) args
used idx (App _ f _ a) = used idx f || used idx a
used idx (As _ _ pat) = used idx pat
used idx (TDelayed _ _ tm) = used idx tm
used idx (TDelay _ _ tm) = used idx tm
used idx (TDelay _ _ _ tm) = used idx tm
used idx (TForce _ tm) = used idx tm
used idx _ = False
@ -169,33 +169,15 @@ mutual
unelabTy' umode env (TDelayed fc r tm)
= do (tm', ty) <- unelabTy' umode env tm
defs <- get Ctxt
case laziness (options defs) of
Nothing => pure (tm', Erased fc)
Just lnames =>
pure (IApp fc
(IApp fc (IVar fc (delayType lnames))
(Implicit fc False))
tm', Erased fc)
unelabTy' umode env (TDelay fc r tm)
pure (IDelayed fc r tm', Erased fc)
unelabTy' umode env (TDelay fc r _ tm)
= do (tm', ty) <- unelabTy' umode env tm
defs <- get Ctxt
case laziness (options defs) of
Nothing => pure (tm', Erased fc)
Just lnames =>
pure (IApp fc
(IImplicitApp fc (IVar fc (delay lnames))
Nothing (Implicit fc False))
tm', Erased fc)
pure (IDelay fc tm', Erased fc)
unelabTy' umode env (TForce fc tm)
= do (tm', ty) <- unelabTy' umode env tm
defs <- get Ctxt
case laziness (options defs) of
Nothing => pure (tm', Erased fc)
Just lnames =>
pure (IApp fc
(IImplicitApp fc (IVar fc (delay lnames))
Nothing (Implicit fc False))
tm', Erased fc)
pure (IForce fc tm', Erased fc)
unelabTy' umode env (PrimVal fc c) = pure (IPrimVal fc c, Erased fc)
unelabTy' umode env (Erased fc) = pure (Implicit fc False, Erased fc)
unelabTy' umode env (TType fc) = pure (IType fc, TType fc)

1
tests/Main.idr
View File

@ -9,6 +9,7 @@ ttimpTests
= ["basic001", "basic002", "basic003", "basic004", "basic005",
"basic006", "basic007",
"eta001", "eta002",
"lazy001",
"nest001", "nest002",
"perf001", "perf002", "perf003",
"qtt001", "qtt002", "qtt003"]

26
tests/ttimp/lazy001/Lazy.yaff Normal file
View File

@ -0,0 +1,26 @@
data Nat : Type where
Z : Nat
S : Nat -> Nat
namespace Stream
data Stream : Type -> Type where
Cons : $a -> Inf (Stream $a) -> Stream $a
ones : Stream Integer
ones = Cons 1 (Delay ones)
countFrom : Integer -> Stream Integer
countFrom $x = Cons x (Delay (countFrom (prim__add_Integer 1 x)))
data List : Type -> Type where
Nil : List $a
Cons : $a -> List $a -> List $ a
take : Nat -> Stream $a -> List $a
take Z $xs = Nil
take (S $k) (Cons $x $xs) = Cons x (take k (Force xs))
every2nd : Nat -> Stream $a -> List $a
every2nd Z $xs = Nil
every2nd (S $k) (Cons _ (Delay (Cons $x $xs))) = Cons x (every2nd k (Force xs))

25
tests/ttimp/lazy001/LazyInf.yaff Normal file
View File

@ -0,0 +1,25 @@
data Nat : Type where
Z : Nat
S : Nat -> Nat
namespace Stream
data Stream : Type -> Type where
Cons : $a -> Inf (Stream $a) -> Stream $a
ones : Stream Integer
ones = Cons 1 ones
countFrom : Integer -> Stream Integer
countFrom $x = Cons x (countFrom (prim__add_Integer 1 x))
data List : Type -> Type where
Nil : List $a
Cons : $a -> List $a -> List $ a
take : Nat -> Stream $a -> List $a
take Z $xs = Nil
take (S $k) (Cons $x $xs) = Cons x (take k xs)
every2nd : Nat -> Stream $a -> List $a
every2nd Z $xs = Nil
every2nd (S $k) (Cons _ (Cons $x $xs)) = Cons x (every2nd k xs)

21
tests/ttimp/lazy001/expected Normal file
View File

@ -0,0 +1,21 @@
Processing as TTImp
Written TTC
Yaffle> (((Main.Stream.Cons [Just a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Cons [Just a = Integer]) 2) (((Main.Cons [Just a = Integer]) 4) (((Main.Cons [Just a = Integer]) 6) (Main.Nil [Just a = Integer]))))
Yaffle> Bye for now!
Processing as TTImp
Written TTC
Yaffle> (((Main.Stream.Cons [Just a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Cons [Just a = Integer]) 2) (((Main.Cons [Just a = Integer]) 4) (((Main.Cons [Just a = Integer]) 6) (Main.Nil [Just a = Integer]))))
Yaffle> Bye for now!
Processing as TTC
Read 0 holes
Read 0 guesses
Read 0 constraints
Read TTC
Yaffle> (((Main.Stream.Cons [Just a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Cons [Just a = Integer]) 2) (((Main.Cons [Just a = Integer]) 4) (((Main.Cons [Just a = Integer]) 6) (Main.Nil [Just a = Integer]))))
Yaffle> Bye for now!

4
tests/ttimp/lazy001/input Normal file
View File

@ -0,0 +1,4 @@
ones
take (S (S (S Z))) ones
every2nd (S (S (S Z))) (countFrom 1)
:q

5
tests/ttimp/lazy001/run Executable file
View File

@ -0,0 +1,5 @@
$1 Lazy.yaff < input
$1 LazyInf.yaff < input
$1 build/LazyInf.ttc < input
rm -rf build

1
yaffle.ipkg
View File

@ -48,6 +48,7 @@ modules =
TTImp.Elab.Check,
TTImp.Elab.Hole,
TTImp.Elab.ImplicitBind,
TTImp.Elab.Lazy,
TTImp.Elab.Local,
TTImp.Elab.Prim,
TTImp.Elab.Term,