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

First attempt at linearity checking pass

Browse Source 
This slows things down a bit because to find the holes and give them the
right multiplicities, we need to normalise all the arguments which might
have been metavariables. Maybe we should skip this if we're not using
anything linear, for efficiency?

As patterns are handled by deciding which side of the as is considered
'used'. In case blocks, that should be the variable name, but in general
it should be the pattern, so IAs now has a flag to say which one.
This commit is contained in:
Edwin Brady 2019-05-19 20:24:14 +01:00
parent 9bd063bbd5
commit 8081b0374a
37 changed files with 1016 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
src/Core/Context.idr
View File

@ -405,6 +405,7 @@ record GlobalDef where
-- placeholder for a yet to be elaborated arguments, but
-- not for implicits because that'd indicate failing the
-- occurs check)
linearChecked : Bool -- Flag whether we've already checked its linearity
definition : Def
export
@ -435,16 +436,17 @@ TTC GlobalDef where
refsList <- fromBuf r b;
let refs = fromList (map (\x => (x, ())) refsList)
c <- fromBuf r b
pure (MkGlobalDef loc name ty mul vis tot fl refs c def)
pure (MkGlobalDef loc name ty mul vis
tot fl refs c True def)
else do let fc = emptyFC
pure (MkGlobalDef fc name (Erased fc)
RigW Public unchecked [] empty
False def)
False True def)
export
newDef : FC -> Name -> RigCount -> ClosedTerm -> Visibility -> Def -> GlobalDef
newDef fc n rig ty vis def
= MkGlobalDef fc n ty rig vis unchecked [] empty False def
= MkGlobalDef fc n ty rig vis unchecked [] empty False False def
public export
record Defs where
@ -512,7 +514,7 @@ addBuiltin : {auto x : Ref Ctxt Defs} ->
PrimFn arity -> Core ()
addBuiltin n ty tot op
= do addDef n (MkGlobalDef emptyFC n ty RigW Public tot
[Inline] empty False (Builtin op))
[Inline] empty False True (Builtin op))
pure ()
export
@ -527,6 +529,28 @@ updateDef n fdef
Just def' => do addDef n (record { definition = def' } gdef)
pure ()
export
updateTy : {auto c : Ref Ctxt Defs} ->
Int -> ClosedTerm -> Core ()
updateTy i ty
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => pure ()
addDef (Resolved i) (record { type = ty } gdef)
pure ()
-- Record that the name has been linearity checked so we don't need to do
-- it again
export
setLinearCheck : {auto c : Ref Ctxt Defs} ->
Int -> Bool -> Core ()
setLinearCheck i chk
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => pure ()
addDef (Resolved i) (record { linearChecked = chk } gdef)
pure ()
export
setCtxt : {auto c : Ref Ctxt Defs} -> Context GlobalDef -> Core ()
setCtxt gam
@ -874,6 +898,12 @@ inCurrentNS : {auto c : Ref Ctxt Defs} ->
inCurrentNS (UN n)
= do defs <- get Ctxt
pure (NS (currentNS defs) (UN n))
inCurrentNS n@(CaseBlock _ _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n@(WithBlock _ _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n@(MN _ _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)

659
src/Core/LinearCheck.idr Normal file
View File

@ -0,0 +1,659 @@
module Core.LinearCheck
import Core.CaseTree
import Core.Context
import Core.Core
import Core.Env
import Core.Normalise
import Core.Options
import Core.UnifyState
import Core.Value
import Core.TT
%default covering
-- List of variable usages - we'll count the contents of specific variables
-- when discharging binders, to ensure that linear names are only used once
data Usage : List Name -> Type where
Nil : Usage vars
(::) : Var vars -> Usage vars -> Usage vars
Show (Usage vars) where
show xs = "[" ++ showAll xs ++ "]"
where
showAll : Usage vs -> String
showAll [] = ""
showAll [el] = show el
showAll (x :: xs) = show x ++ ", " ++ show xs
Weaken Usage where
weaken [] = []
weaken (MkVar x :: xs) = MkVar (Later x) :: weaken xs
doneScope : Usage (n :: vars) -> Usage vars
doneScope [] = []
doneScope (MkVar First :: xs) = doneScope xs
doneScope (MkVar (Later p) :: xs) = MkVar p :: doneScope xs
(++) : Usage ns -> Usage ns -> Usage ns
(++) [] ys = ys
(++) (x :: xs) ys = x :: xs ++ ys
count : Nat -> Usage ns -> Nat
count p [] = 0
count p (v :: xs)
= if p == varIdx v then 1 + count p xs else count p xs
localPrf : {later : _} -> Var (later ++ n :: vars)
localPrf {later = []} = MkVar First
localPrf {n} {vars} {later = (x :: xs)}
= let MkVar p = localPrf {n} {vars} {later = xs} in
MkVar (Later p)
mutual
updateHoleUsageArgs : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> List (Term vars) -> Core Bool
updateHoleUsageArgs useInHole var [] = pure False
updateHoleUsageArgs useInHole var (a :: as)
= do h <- updateHoleUsage useInHole var a
h' <- updateHoleUsageArgs useInHole var as
pure (h || h')
-- The assumption here is that hole types are abstracted over the entire
-- environment, so that they have the appropriate number of function
-- arguments and lets are still in the right place
updateHoleType : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> Term vs -> List (Term vars) ->
Core (Term vs)
updateHoleType useInHole var (Bind bfc nm (Pi c e ty) sc) (Local _ r v _ :: as)
-- if the argument to the hole type is the variable of interest,
-- and the variable should be used in the hole, set it to Rig1,
-- otherwise set it to Rig0
= if varIdx var == v
then do scty <- updateHoleType False var sc as
let c' = if useInHole then c else Rig0
pure (Bind bfc nm (Pi c' e ty) scty)
else do scty <- updateHoleType useInHole var sc as
pure (Bind bfc nm (Pi c e ty) scty)
updateHoleType useInHole var (Bind bfc nm (Let c val ty) sc) as
= case val of
Local _ r v _
=> if varIdx var == v
then do scty <- updateHoleType False var sc as
let c' = if useInHole then c else Rig0
pure (Bind bfc nm (Let c' val ty) scty)
else do scty <- updateHoleType False var sc as
pure (Bind bfc nm (Let c val ty) scty)
_ => do scty <- updateHoleType False var sc as
pure (Bind bfc nm (Let c val ty) scty)
updateHoleType useInHole var (Bind bfc nm (Pi c e ty) sc) (a :: as)
= do updateHoleUsage False var a
scty <- updateHoleType useInHole var sc as
pure (Bind bfc nm (Pi c e ty) scty)
updateHoleType useInHole var ty as
= do updateHoleUsageArgs False var as
pure ty
updateHoleUsagePats : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> List (Term vars) ->
(vs ** (Env Term vs, Term vs, Term vs)) ->
Core Bool
updateHoleUsagePats {vars} useInHole var args (vs ** (env, lhs, rhs))
= do -- Find the argument which corresponds to var
let argpos = findArg Z args
log 10 $ "At positions " ++ show argpos
-- Find what it's position is in env by looking at the lhs args
let vars = mapMaybe (findLocal (map snd (getArgs lhs))) argpos
hs <- traverse (\vsel => updateHoleUsage useInHole vsel rhs)
vars
pure (or (map Delay hs))
where
findArg : Nat -> List (Term vars) -> List Nat
findArg i [] = []
findArg i (Local _ _ idx vel :: els)
= if idx == varIdx var
then i :: findArg (1 + i) els
else findArg (1 + i) els
findArg i (_ :: els) = findArg (1 + i) els
findLocal : List (Term vs) -> Nat -> Maybe (Var vs)
findLocal (Local _ _ _ p :: _) Z = Just (MkVar p)
findLocal (_ :: els) (S k) = findLocal els k
findLocal _ _ = Nothing
updateHoleUsage : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> Term vars -> Core Bool
updateHoleUsage useInHole (MkVar var) (Bind _ n (Let c val ty) sc)
= do h <- updateHoleUsage useInHole (MkVar var) val
h' <- updateHoleUsage useInHole (MkVar (Later var)) sc
pure (h || h')
updateHoleUsage useInHole (MkVar var) (Bind _ n b sc)
= updateHoleUsage useInHole (MkVar (Later var)) sc
updateHoleUsage useInHole var (Meta fc n i args)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => updateHoleUsageArgs useInHole var args
-- only update for holes with no definition yet
case definition gdef of
Hole _ =>
do let ty = type gdef
ty' <- updateHoleType useInHole var ty args
updateTy i ty'
pure True
_ => updateHoleUsageArgs useInHole var args
updateHoleUsage useInHole var (As _ a p)
= do h <- updateHoleUsage useInHole var a
h' <- updateHoleUsage useInHole var a
pure (h || h')
updateHoleUsage useInHole var (TDelayed _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TDelay _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TForce _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var tm
= case getFnArgs tm of
(Ref _ _ fn, args) =>
do aup <- updateHoleUsageArgs useInHole var (map snd args)
defs <- get Ctxt
Just (NS _ (CaseBlock _ _), PMDef _ _ _ pats) <-
lookupExactBy (\d => (fullname d, definition d))
fn (gamma defs)
| _ => pure aup
hs <- traverse (updateHoleUsagePats useInHole var (map snd args)) pats
pure (or (aup :: map Delay hs))
(f, []) => pure False
(f, args) => updateHoleUsageArgs useInHole var (f :: map snd args)
-- Linearity checking of an already checked term. This serves two purposes:
-- + Checking correct usage of linear bindings
-- + updating hole types to reflect usage counts correctly
-- Returns term, normalised type, and a list of used variables
mutual
lcheck : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState } ->
RigCount -> (erase : Bool) -> Env Term vars -> Term vars ->
Core (Term vars, Glued vars, Usage vars)
lcheck {vars} rig erase env (Local {name} fc x idx prf)
= let b = getBinder prf env
rigb = multiplicity b
ty = binderType b in
do when (not erase) $ rigSafe rigb rig
pure (Local fc x idx prf, gnf env ty, used rig)
where
getName : {idx : _} -> (vs : List Name) -> .(IsVar n idx vs) -> Name
getName (x :: _) First = x
getName (x :: xs) (Later p) = getName xs p
rigSafe : RigCount -> RigCount -> Core ()
rigSafe Rig1 RigW = throw (LinearMisuse fc (getName vars prf) Rig1 RigW)
rigSafe Rig0 RigW = throw (LinearMisuse fc (getName vars prf) Rig0 RigW)
rigSafe Rig0 Rig1 = throw (LinearMisuse fc (getName vars prf) Rig0 Rig1)
rigSafe _ _ = pure ()
-- count the usage if we're in a linear context. If not, the usage doesn't
-- matter
used : RigCount -> Usage vars
used Rig1 = [MkVar prf]
used _ = []
lcheck rig erase env (Ref fc nt fn)
= do ty <- lcheckDef rig erase env fn
pure (Ref fc nt fn, gnf env (embed ty), [])
-- If the meta has a definition, and we're not in Rig0, expand it first
-- and check the result.
-- Otherwise, don't count variable usage in holes, so as far as linearity
-- checking is concerned, update the type so that the binders
-- are in Rig0
lcheck {vars} rig erase env (Meta fc n idx args)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| _ => throw (UndefinedName fc n)
let expand = case (definition gdef, rig) of
(Hole _, _) => False
(_, Rig0) => False
_ => True
if expand
then expandMeta rig erase env n idx (definition gdef) args
else do let ty : ClosedTerm
= case definition gdef of
Hole _ => unusedHoleArgs args (type gdef)
_ => type gdef
nty <- nf defs env (embed ty)
lcheckMeta rig erase env fc n idx args [] nty
where
unusedHoleArgs : List a -> Term vs -> Term vs
unusedHoleArgs (_ :: args) (Bind bfc n (Pi _ e ty) sc)
= Bind bfc n (Pi Rig0 e ty) (unusedHoleArgs args sc)
unusedHoleArgs _ ty = ty
lcheck rig_in erase env (Bind fc nm b sc)
= do (b', bt, usedb) <- lcheckBinder rig erase env b
(sc', sct, usedsc) <- lcheck rig erase (b' :: env) sc
defs <- get Ctxt
let used_in = count 0 usedsc
holeFound <- if not erase && isLinear (multiplicity b)
then updateHoleUsage (used_in == 0) (MkVar First) sc'
else pure False
-- if there's a hole, assume it will contain the missing usage
-- if there is none already
let used = case rigMult (multiplicity b) rig of
Rig1 => if holeFound && used_in == 0
then 1
else used_in
_ => used_in
when (not erase) $
checkUsageOK used (rigMult (multiplicity b) rig)
defs <- get Ctxt
discharge defs env fc nm b' bt sc' sct (usedb ++ doneScope usedsc)
where
rig : RigCount
rig = case b of
Pi _ _ _ => Rig0
_ => rig_in
checkUsageOK : Nat -> RigCount -> Core ()
checkUsageOK used Rig0 = pure ()
checkUsageOK used RigW = pure ()
checkUsageOK used Rig1
= if used == 1
then pure ()
else throw (LinearUsed fc used nm)
lcheck rig erase env (App fc f p a)
= do (f', gfty, fused) <- lcheck rig erase env f
defs <- get Ctxt
fty <- getNF gfty
case fty of
NBind _ _ (Pi rigf _ ty) scdone =>
-- if the argument is borrowed, it's okay to use it in
-- unrestricted context, because we'll be out of the
-- application without spending it
do let checkRig = rigMult rigf rig
(a', gaty, aused) <- lcheck checkRig erase env a
sc' <- scdone defs (toClosure defaultOpts env a')
let aerased = if erase && rigf == Rig0 then Erased fc else a'
-- Possibly remove this check, or make it a compiler
-- flag? It is a useful double check on the result of
-- elaboration, but there are pathological cases where
-- it makes the check very slow (id id id id ... id id etc
-- for example) and there may be similar realistic cases.
-- If elaboration is correct, this should never fail!
-- when (not (convert gam env aty ty)) $
-- throw (CantConvert loc env (quote (noGam gam) env ty)
-- (quote (noGam gam) env aty))
pure (App fc f' p aerased,
glueBack defs env sc',
fused ++ aused)
_ => do tfty <- getTerm gfty
throw (InternalError ("Linearity checking failed on " ++ show f' ++
" (" ++ show tfty ++ " not a function type)"))
lcheck rig erase env (As fc as pat)
= do (as', _, _) <- lcheck rig erase env as
(pat', pty, u) <- lcheck rig erase env pat
pure (As fc as' pat', pty, u)
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
ty <- getTerm gty
pure (TDelay fc r 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
=> 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)
= pure (PrimVal fc c, gErased fc, [])
lcheck rig erase env (Erased fc)
= pure (Erased fc, gErased fc, [])
lcheck rig erase env (TType fc)
= pure (TType fc, gType fc, [])
lcheckBinder : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
RigCount -> (erase : Bool) -> Env Term vars ->
Binder (Term vars) ->
Core (Binder (Term vars), Glued vars, Usage vars)
lcheckBinder rig erase env (Lam c x ty)
= do (tyv, tyt, _) <- lcheck Rig0 erase env ty
pure (Lam c x tyv, tyt, [])
lcheckBinder rig erase env (Let rigc val ty)
= do (tyv, tyt, _) <- lcheck Rig0 erase env ty
(valv, valt, vs) <- lcheck (rigMult rig rigc) erase env val
pure (Let rigc valv tyv, tyt, vs)
lcheckBinder rig erase env (Pi c x ty)
= do (tyv, tyt, _) <- lcheck Rig0 erase env ty
pure (Pi c x tyv, tyt, [])
lcheckBinder rig erase env (PVar c ty)
= do (tyv, tyt, _) <- lcheck Rig0 erase env ty
pure (PVar c tyv, tyt, [])
lcheckBinder rig erase env (PLet rigc val ty)
= do (tyv, tyt, _) <- lcheck Rig0 erase env ty
(valv, valt, vs) <- lcheck (rigMult rig rigc) erase env val
pure (PLet rigc valv tyv, tyt, vs)
lcheckBinder rig erase env (PVTy c ty)
= do (tyv, tyt, _) <- lcheck Rig0 erase env ty
pure (PVTy c tyv, tyt, [])
discharge : Defs -> Env Term vars ->
FC -> (nm : Name) -> Binder (Term vars) -> Glued vars ->
Term (nm :: vars) -> Glued (nm :: vars) -> Usage vars ->
Core (Term vars, Glued vars, Usage vars)
discharge defs env fc nm (Lam c x ty) gbindty scope gscopety used
= do scty <- getTerm gscopety
pure (Bind fc nm (Lam c x ty) scope,
gnf env (Bind fc nm (Pi c x ty) scty), used)
discharge defs env fc nm (Let c val ty) gbindty scope gscopety used
= do scty <- getTerm gscopety
pure (Bind fc nm (Let c val ty) scope,
gnf env (Bind fc nm (Let c val ty) scty), used)
discharge defs env fc nm (Pi c x ty) gbindty scope gscopety used
= pure (Bind fc nm (Pi c x ty) scope, gbindty, used)
discharge defs env fc nm (PVar c ty) gbindty scope gscopety used
= do scty <- getTerm gscopety
pure (Bind fc nm (PVar c ty) scope,
gnf env (Bind fc nm (PVTy c ty) scty), used)
discharge defs env fc nm (PLet c val ty) gbindty scope gscopety used
= do scty <- getTerm gscopety
pure (Bind fc nm (PLet c val ty) scope,
gnf env (Bind fc nm (PLet c val ty) scty), used)
discharge defs env fc nm (PVTy c ty) gbindty scope gscopety used
= pure (Bind fc nm (PVTy c ty) scope, gbindty, used)
data ArgUsage
= UseAny -- RigW so we don't care
| Use0 -- argument position not used
| Use1 -- argument position used exactly once
| UseKeep -- keep as is
| UseUnknown -- hole, so can't tell
Show ArgUsage where
show UseAny = "any"
show Use0 = "0"
show Use1 = "1"
show UseKeep = "keep"
show UseUnknown = "unknown"
-- Check argument usage in case blocks. Returns a list of how each argument
-- in the case block is used, to build the appropriate type for the outer
-- block.
getArgUsage : {auto c : Ref Ctxt Defs} ->
{auto e : Ref UST UState} ->
FC -> RigCount -> ClosedTerm ->
List (vs ** (Env Term vs, Term vs, Term vs)) ->
Core (List ArgUsage)
getArgUsage topfc rig ty pats
= do us <- traverse (getPUsage ty) pats
pure (map snd !(combine us))
where
getCaseUsage : Term ns -> Env Term vs -> List (Term vs) ->
Usage vs -> Term vs ->
Core (List (Name, ArgUsage))
getCaseUsage (Bind _ n (Pi Rig1 e ty) sc) env (Local _ _ idx p :: args) used rhs
= do rest <- getCaseUsage sc env args used rhs
let used_in = count idx used
holeFound <- updateHoleUsage (used_in == 0) (MkVar p) rhs
let ause
= if holeFound && used_in == 0
then UseUnknown
else if used_in == 0
then Use0
else Use1
pure ((n, ause) :: rest)
getCaseUsage (Bind _ n (Pi c e ty) sc) env (arg :: args) used rhs
= do rest <- getCaseUsage sc env args used rhs
case c of
Rig0 => pure ((n, Use0) :: rest)
Rig1 => pure ((n, UseKeep) :: rest)
_ => pure ((n, UseKeep) :: rest)
getCaseUsage tm env args used rhs = pure []
checkUsageOK : FC -> Nat -> Name -> Bool -> RigCount -> Core ()
checkUsageOK fc used nm isloc Rig0 = pure ()
checkUsageOK fc used nm isloc RigW = pure ()
checkUsageOK fc used nm True Rig1
= if used > 1
then throw (LinearUsed fc used nm)
else pure ()
checkUsageOK fc used nm isloc Rig1
= if used == 1
then pure ()
else throw (LinearUsed fc used nm)
-- Is the variable one of the lhs arguments; i.e. do we treat it as
-- affine rather than linear
isLocArg : Var vars -> List (Term vars) -> Bool
isLocArg p [] = False
isLocArg p (Local _ _ idx _ :: args)
= if idx == varIdx p
then True
else isLocArg p args
isLocArg p (As _ tm pat :: args)
= isLocArg p (tm :: pat :: args)
isLocArg p (_ :: args) = isLocArg p args
-- As checkEnvUsage in general, but it's okay for local variables to
-- remain unused (since in that case, they must be used outside the
-- case block)
checkEnvUsage : RigCount ->
Env Term vars -> Usage (done ++ vars) ->
List (Term (done ++ vars)) ->
Term (done ++ vars) -> Core ()
checkEnvUsage rig [] usage args tm = pure ()
checkEnvUsage rig {done} {vars = nm :: xs} (b :: env) usage args tm
= do let pos = localPrf {later = done}
let used_in = count (varIdx pos) usage
holeFound <- if isLinear (multiplicity b)
then updateHoleUsage (used_in == 0) pos tm
else pure False
let used = case rigMult (multiplicity b) rig of
Rig1 => if holeFound && used_in == 0
then 1
else used_in
_ => used_in
checkUsageOK (getLoc (binderType b))
used nm (isLocArg pos args)
(rigMult (multiplicity b) rig)
checkEnvUsage {done = done ++ [nm]} rig env
(rewrite sym (appendAssociative done [nm] xs) in usage)
(rewrite sym (appendAssociative done [nm] xs) in args)
(rewrite sym (appendAssociative done [nm] xs) in tm)
getPUsage : ClosedTerm -> (vs ** (Env Term vs, Term vs, Term vs)) ->
Core (List (Name, ArgUsage))
getPUsage ty (_ ** (penv, lhs, rhs))
= do logEnv 10 "Env" penv
logTerm 10 "LHS" lhs
logTerm 10 "RHS" rhs
(rhs', _, used) <- lcheck rig False penv rhs
let args = map snd (getArgs lhs)
checkEnvUsage {done = []} rig penv used args rhs'
getCaseUsage ty penv args used rhs
combineUsage : (Name, ArgUsage) -> (Name, ArgUsage) ->
Core (Name, ArgUsage)
combineUsage (n, Use0) (_, Use1)
= throw (GenericMsg topfc ("Inconsistent usage of " ++ show n ++ " in case branches"))
combineUsage (n, Use1) (_, Use0)
= throw (GenericMsg topfc ("Inconsistent usage of " ++ show n ++ " in case branches"))
combineUsage (n, UseAny) _ = pure (n, UseAny)
combineUsage _ (n, UseAny) = pure (n, UseAny)
combineUsage (n, UseKeep) _ = pure (n, UseKeep)
combineUsage _ (n, UseKeep) = pure (n, UseKeep)
combineUsage (n, UseUnknown) _ = pure (n, UseUnknown)
combineUsage _ (n, UseUnknown) = pure (n, UseUnknown)
combineUsage x y = pure x
combineUsages : List (Name, ArgUsage) -> List (Name, ArgUsage) ->
Core (List (Name, ArgUsage))
combineUsages [] [] = pure []
combineUsages (u :: us) (v :: vs)
= do u' <- combineUsage u v
us' <- combineUsages us vs
pure (u' :: us')
combineUsages _ _ = throw (InternalError "Argument usage lists inconsistent")
combine : List (List (Name, ArgUsage)) ->
Core (List (Name, ArgUsage))
combine [] = pure []
combine [x] = pure x
combine (x :: xs)
= do xs' <- combine xs
combineUsages x xs'
lcheckDef : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
RigCount -> (erase : Bool) -> Env Term vars -> Name ->
Core ClosedTerm
lcheckDef rig True env n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
pure (type def)
lcheckDef rig False env n
= do defs <- get Ctxt
let Just idx = getNameID n (gamma defs)
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
Just def <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
if linearChecked def
then pure (type def)
else case definition def of
PMDef _ _ _ pats =>
do u <- getArgUsage (getLoc (type def))
rig (type def) pats
let ty' = updateUsage u (type def)
updateTy idx ty'
setLinearCheck idx True
pure ty'
_ => pure (type def)
where
updateUsage : List ArgUsage -> Term ns -> Term ns
updateUsage (u :: us) (Bind bfc n (Pi c e ty) sc)
= let sc' = updateUsage us sc
c' = case u of
Use0 => Rig0
Use1 => Rig1 -- ignore usage elsewhere, we checked here
UseUnknown => Rig0 -- don't know, need to update hole types
UseKeep => c -- matched here, so count usage elsewhere
UseAny => c in -- no constraint, so leave alone
Bind bfc n (Pi c' e ty) sc'
updateUsage _ ty = ty
expandMeta : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
RigCount -> (erase : Bool) -> Env Term vars ->
Name -> Int -> Def -> List (Term vars) ->
Core (Term vars, Glued vars, Usage vars)
expandMeta rig erase env n idx (PMDef [] (STerm fn) _ _) args
= do tm <- substMeta (embed fn) args []
lcheck rig erase env tm
where
substMeta : Term (drop ++ vs) -> List (Term vs) -> SubstEnv drop vs ->
Core (Term vs)
substMeta (Bind bfc n (Lam c e ty) sc) (a :: as) env
= substMeta sc as (a :: env)
substMeta rhs [] env = pure (substs env rhs)
substMeta _ _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n))
expandMeta rig erase env n idx _ _
= throw (InternalError ("Badly formed metavar solution " ++ show n))
lcheckMeta : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
RigCount -> Bool -> Env Term vars ->
FC -> Name -> Int ->
(args : List (Term vars)) ->
(checked : List (Term vars)) ->
NF vars -> Core (Term vars, Glued vars, Usage vars)
lcheckMeta rig erase env fc n idx
(arg :: args) chk (NBind _ _ (Pi rigf _ ty) sc)
= do let checkRig = rigMult rigf rig
(arg', gargTy, aused) <- lcheck checkRig erase env arg
defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts env arg')
let aerased = if erase && rigf == Rig0 then Erased fc else arg'
(tm, gty, u) <- lcheckMeta rig erase env fc n idx args
(aerased :: chk) sc'
pure (tm, gty, aused ++ u)
lcheckMeta rig erase env fc n idx (arg :: args) chk nty
= do defs <- get Ctxt
empty <- clearDefs defs
ty <- quote empty env nty
throw (InternalError ("Linearity checking failed on metavar
" ++ show n ++ " (" ++ show ty ++
" not a function type)"))
lcheckMeta rig erase env fc n idx [] chk nty
= do defs <- get Ctxt
pure (Meta fc n idx (reverse chk), glueBack defs env nty, [])
checkEnvUsage : {done : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
Env Term vars -> Usage (done ++ vars) ->
Term (done ++ vars) ->
Core ()
checkEnvUsage fc rig [] usage tm = pure ()
checkEnvUsage fc rig {done} {vars = nm :: xs} (b :: env) usage tm
= do let pos = localPrf {later = done}
let used_in = count (varIdx pos) usage
holeFound <- if isLinear (multiplicity b)
then updateHoleUsage (used_in == 0) pos tm
else pure False
let used = case rigMult (multiplicity b) rig of
Rig1 => if holeFound && used_in == 0
then 1
else used_in
_ => used_in
checkUsageOK used (rigMult (multiplicity b) rig)
checkEnvUsage {done = done ++ [nm]} fc rig env
(rewrite sym (appendAssociative done [nm] xs) in usage)
(rewrite sym (appendAssociative done [nm] xs) in tm)
where
checkUsageOK : Nat -> RigCount -> Core ()
checkUsageOK used Rig0 = pure ()
checkUsageOK used RigW = pure ()
checkUsageOK used Rig1
= if used == 1
then pure ()
else throw (LinearUsed fc used nm)
-- Linearity check an elaborated term. If 'erase' is set, erase anything that's in
-- a Rig0 argument position (we can't do this until typechecking is complete, though,
-- since it might be used for unification/reasoning elsewhere, so we only do this for
-- definitions ready for compilation).
export
linearCheck : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount -> (erase : Bool) ->
Env Term vars -> Term vars ->
Core (Term vars)
linearCheck fc rig erase env tm
= do logTerm 5 "Linearity check on " tm
(tm', _, used) <- lcheck rig erase env tm
when (not erase) $ checkEnvUsage {done = []} fc rig env used tm'
pure tm'

12
src/Core/Normalise.idr
View File

@ -68,7 +68,7 @@ parameters (defs : Defs, topopts : EvalOpts)
eval env locs (Bind fc x (Lam r _ ty) scope) ((p, thunk) :: stk)
= eval env (thunk :: locs) scope stk
eval env locs (Bind fc x b@(Let r val ty) scope) stk
= if holesOnly topopts
= if holesOnly topopts || argHolesOnly topopts
then do b' <- traverse (\tm => eval env locs tm stk) b
pure $ NBind fc x b'
(\defs', arg => evalWithOpts defs' topopts
@ -109,7 +109,7 @@ parameters (defs : Defs, topopts : EvalOpts)
evalLocal {vars = []} env locs fc mrig idx prf stk
= case getBinder prf env of
Let _ val _ =>
if not (holesOnly topopts)
if not (holesOnly topopts || argHolesOnly topopts)
then eval env [] val stk
else pure $ NApp fc (NLocal mrig idx prf) stk
_ => pure $ NApp fc (NLocal mrig idx prf) stk
@ -758,12 +758,14 @@ logEnv lvl msg env
where
dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
dumpEnv [] = pure ()
dumpEnv {vs = x :: _} (Let _ val ty :: bs)
dumpEnv {vs = x :: _} (Let c val ty :: bs)
= do logTermNF lvl (msg ++ ": let " ++ show x) bs val
logTermNF lvl (msg ++ ":" ++ show x) bs ty
logTermNF lvl (msg ++ ":" ++ show c ++ " " ++
show x) bs ty
dumpEnv bs
dumpEnv {vs = x :: _} (b :: bs)
= do logTermNF lvl (msg ++ ":" ++ show x) bs (binderType b)
= do logTermNF lvl (msg ++ ":" ++ show (multiplicity b) ++ " " ++
show x) bs (binderType b)
dumpEnv bs

17
src/Core/TT.idr
View File

@ -310,6 +310,14 @@ export
sameVar : Var xs -> Var xs -> Bool
sameVar (MkVar {i=x} _) (MkVar {i=y} _) = x == y
export
varIdx : Var xs -> Nat
varIdx (MkVar {i} _) = i
export
Show (Var ns) where
show (MkVar {n} _) = show n
public export
record AppInfo where
constructor MkAppInfo
@ -871,6 +879,7 @@ resolveNames vars tm = tm
-- Substitute some explicit terms for names in a term, and remove those
-- names from the scope
namespace SubstEnv
public export
data SubstEnv : List Name -> List Name -> Type where
Nil : SubstEnv [] vars
(::) : Term vars ->
@ -914,6 +923,10 @@ namespace SubstEnv
substEnv env (Erased fc) = Erased fc
substEnv env (TType fc) = TType fc
export
substs : SubstEnv drop vars -> Term (drop ++ vars) -> Term vars
substs env tm = substEnv {outer = []} env tm
export
subst : Term vars -> Term (x :: vars) -> Term vars
subst val tm = substEnv {outer = []} {drop = [_]} [val] tm
@ -1007,8 +1020,8 @@ export Show (Term vars) where
= "let " ++ showCount c ++ show x ++ " : " ++ show ty ++
" = " ++ show val ++ " in " ++ show sc
showApp (Bind _ x (Pi c Explicit ty) sc) []
= "(" ++ showCount c ++ show x ++ " : " ++ show ty ++
") -> " ++ show sc
= "((" ++ showCount c ++ show x ++ " : " ++ show ty ++
") -> " ++ show sc ++ ")"
showApp (Bind _ x (Pi c Implicit ty) sc) []
= "{" ++ showCount c ++ show x ++ " : " ++ show ty ++
"} -> " ++ show sc

7
src/Core/UnifyState.idr
View File

@ -4,6 +4,7 @@ import Core.Context
import Core.Core
import Core.Env
import Core.FC
import Core.Normalise
import Core.TT
import Core.TTC
import Utils.Binary
@ -120,12 +121,13 @@ genVarName str
-- Again, for case names
export
genCaseName : {auto u : Ref UST UState} ->
genCaseName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Int -> Core Name
genCaseName root
= do ust <- get UST
put UST (record { nextName $= (+1) } ust)
pure (CaseBlock root (nextName ust))
inCurrentNS (CaseBlock root (nextName ust))
addHoleName : {auto u : Ref UST UState} ->
FC -> Name -> Int -> Core ()
@ -328,6 +330,7 @@ newMeta {vars} fc rig env n ty nocyc
let hole = record { noCycles = nocyc }
(newDef fc n rig hty Public (Hole False))
log 5 $ "Adding new meta " ++ show (n, fc, rig)
logTerm 10 ("New meta type " ++ show n) hty
idx <- addDef n hole
addHoleName fc n idx
pure (idx, Meta fc n idx envArgs)

44
src/TTImp/Elab.idr
View File

@ -3,6 +3,7 @@ module TTImp.Elab
import Core.Context
import Core.Core
import Core.Env
import Core.LinearCheck
import Core.Normalise
import Core.UnifyState
import Core.Unify
@ -27,7 +28,7 @@ elabTermSub : {vars : _} ->
NestedNames vars -> Env Term vars ->
Env Term inner -> SubVars inner vars ->
RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
Core (Term vars, Term vars, Glued vars)
elabTermSub defining mode opts nest env env' sub tm ty
= do let incase = elem InCase opts
let holesokay = elem HolesOkay opts
@ -58,6 +59,8 @@ elabTermSub defining mode opts nest env env' sub tm ty
do ust <- get UST
put UST (record { delayedElab = [] } ust)
throw err)
defs <- get Ctxt
chktm <- normaliseArgHoles defs env chktm
-- As long as we're not in a case block, finish off constraint solving
when (not incase) $
-- resolve any default hints
@ -67,22 +70,34 @@ elabTermSub defining mode opts nest env env' sub tm ty
-- helpful errors.
solveConstraints solvemode LastChance
-- Linearity and hole checking.
-- on the LHS, all holes need to have been solved
case mode of
InLHS _ => checkUserHoles True
chktm <- case mode of
InLHS _ => do checkUserHoles True
pure chktm
-- elsewhere, all unification problems must be
-- solved, though we defer that if it's a case block since we
-- might learn a bit more later
_ => when (not incase) $
checkNoGuards
-- might learn a bit more later.
_ => if (not incase)
then do checkNoGuards
linearCheck (getFC tm) rigc False env chktm
-- Linearity checking looks in case blocks, so no
-- need to check here.
else pure chktm
-- Put the current hole state back to what it was (minus anything
-- which has been solved in the meantime)
when (not incase) $
do hs <- getHoles
restoreHoles (addHoles empty hs (toList oldhs))
pure (chktm, chkty)
-- On the RHS, erase everything in a 0-multiplicity position
-- (This doesn't do a full linearity check, just erases by
-- type)
chkErase <- case mode of
InExpr => linearCheck (getFC tm) rigc True env chktm
_ => pure chktm
pure (chktm, chkErase, chkty)
where
addHoles : (acc : IntMap (FC, Name)) ->
(allHoles : IntMap (FC, Name)) ->
@ -101,7 +116,7 @@ elabTerm : {vars : _} ->
Int -> ElabMode -> List ElabOpt ->
NestedNames vars -> Env Term vars ->
RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
Core (Term vars, Term vars, Glued vars)
elabTerm defining mode opts nest env tm ty
= elabTermSub defining mode opts nest env env SubRefl tm ty
@ -113,11 +128,12 @@ checkTermSub : {vars : _} ->
NestedNames vars -> Env Term vars ->
Env Term inner -> SubVars inner vars ->
RawImp -> Glued vars ->
Core (Term vars)
Core (Term vars, Term vars)
checkTermSub defining mode opts nest env env' sub tm ty
= do (tm_elab, _) <- elabTermSub defining mode opts nest
env env' sub tm (Just ty)
pure tm_elab
= do (tm_elab, tm_erase, _) <-
elabTermSub defining mode opts nest
env env' sub tm (Just ty)
pure (tm_elab, tm_erase)
export
checkTerm : {vars : _} ->
@ -126,6 +142,6 @@ checkTerm : {vars : _} ->
Int -> ElabMode -> List ElabOpt ->
NestedNames vars -> Env Term vars ->
RawImp -> Glued vars ->
Core (Term vars)
Core (Term vars, Term vars)
checkTerm defining mode opts nest env tm ty
= checkTermSub defining mode opts nest env env SubRefl tm ty

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

@ -120,7 +120,7 @@ mutual
fnty <- sc defs (toClosure defaultOpts env metaval)
when (bindingVars elabinfo) $
do est <- get EST
put EST (addBindIfUnsolved nm rig env metaval metaty est)
put EST (addBindIfUnsolved nm argRig env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty expargs impargs kr expty
@ -188,8 +188,11 @@ mutual
-- *may* have as patterns in it and we need to retain them.
-- (As patterns are a bit of a hack but I don't yet see a
-- better way that leads to good code...)
[] <- convert fc elabinfo env (gnf env metaval)
(gnf env argv)
[] <- handle
(convert fc elabinfo env (gnf env metaval)
(gnfOpts withHoles (letToLam env) argv))
(\err => convert fc elabinfo env (gnf env metaval)
(gnf env argv))
| cs => throw (CantConvert fc env metaval argv)
case elabMode elabinfo of
InLHS _ => -- reset hole and redo it with the unexpanded definition

30
src/TTImp/Elab/As.idr
View File

@ -23,9 +23,9 @@ checkAs : {vars : _} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> Name -> RawImp -> Maybe (Glued vars) ->
FC -> UseSide -> Name -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkAs rig elabinfo nest env fc n_in pat topexp
checkAs rig elabinfo nest env fc side n_in pat topexp
= do let elabmode = elabMode elabinfo
let InLHS _ = elabmode
| _ => throw (GenericMsg fc "@-patterns only allowed in pattern clauses")
@ -39,19 +39,37 @@ checkAs rig elabinfo nest env fc n_in pat topexp
notePatVar n
case lookup n (boundNames est) of
Nothing =>
do (pattm, patty) <- checkImp rig elabinfo nest env pat topexp
do (pattm, patty) <- checkImp rigPat elabinfo nest env pat topexp
(tm, exp, bty) <- mkPatternHole fc rig n env
(implicitMode elabinfo)
topexp
log 5 $ "Added as pattern name " ++ show (n, (tm, exp, bty))
log 5 $ "Added as pattern name " ++ show (n, (rigAs, tm, exp, bty))
defs <- get Ctxt
est <- get EST
put EST
(record { boundNames $= ((n, AsBinding tm exp pattm) :: ),
toBind $= ((n, AsBinding tm bty pattm) ::) }
(record { boundNames $= ((n, AsBinding rigAs tm exp pattm) :: ),
toBind $= ((n, AsBinding rigAs tm bty pattm) ::) }
est)
-- addNameType loc (UN str) env exp
(ntm, nty) <- checkExp rig elabinfo env fc tm (gnf env exp)
(Just patty)
pure (As fc ntm pattm, patty)
Just bty => throw (NonLinearPattern fc n_in)
where
-- Only one side can be usable if it's linear! Normally we'd assume this
-- to be the new variable (UseRight), but in generated case blocks it's
-- better if it's the pattern (UseLeft)
rigPat' : UseSide -> RigCount
rigPat' UseLeft = if rig == Rig1 then Rig1 else rig
rigPat' UseRight = if rig == Rig1 then Rig0 else rig
rigPat : RigCount
rigPat = rigPat' side
rigAs' : UseSide -> RigCount
rigAs' UseLeft = if rig == Rig1 then Rig0 else rig
rigAs' UseRight = if rig == Rig1 then Rig1 else rig
rigAs : RigCount
rigAs = rigAs' side

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

@ -172,15 +172,15 @@ allow (Just (MkVar p)) env = toRig1 p env
shrinkImp : SubVars outer vars ->
(Name, ImplBinding vars) -> Maybe (Name, ImplBinding outer)
shrinkImp sub (n, NameBinding tm ty)
shrinkImp sub (n, NameBinding c tm ty)
= do tm' <- shrinkTerm tm sub
ty' <- shrinkTerm ty sub
pure (n, NameBinding tm' ty')
shrinkImp sub (n, AsBinding tm ty pat)
pure (n, NameBinding c tm' ty')
shrinkImp sub (n, AsBinding c tm ty pat)
= do tm' <- shrinkTerm tm sub
ty' <- shrinkTerm ty sub
pat' <- shrinkTerm pat sub
pure (n, AsBinding tm' ty' pat')
pure (n, AsBinding c tm' ty' pat')
findImpsIn : FC -> Env Term vars -> List (Name, Term vars) -> Term vars ->
Core ()
@ -404,7 +404,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
addEnv {vs = v :: vs} (b :: bs) (DropCons p) used
= let (rest, used') = addEnv bs p used in
case canBindName v used' of
Just n => (Just (IAs fc n (Implicit fc True)) :: rest, n :: used')
Just n => (Just (IAs fc UseLeft n (Implicit fc True)) :: rest, n :: used')
_ => (Just (Implicit fc True) :: rest, used')
-- Replace a variable in the argument list; if the reference is to
@ -415,7 +415,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
List RawImp
replace First lhs (old :: xs)
= let lhs' = case old of
Just (IAs loc' n _) => IAs loc' n lhs
Just (IAs loc' side n _) => IAs loc' side n lhs
_ => lhs in
lhs' :: mapMaybe id xs
replace (Later p) lhs (Nothing :: xs)
@ -436,7 +436,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
usedIn : RawImp -> List Name
usedIn (IBindVar _ n) = [UN n]
usedIn (IApp _ f a) = usedIn f ++ usedIn a
usedIn (IAs _ n a) = n :: usedIn a
usedIn (IAs _ _ n a) = n :: usedIn a
usedIn (IAlternative _ _ alts) = concatMap usedIn alts
usedIn _ = []

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

@ -35,21 +35,21 @@ Eq ElabOpt where
-- or a binding of an @-pattern which has an associated pattern.
public export
data ImplBinding : List Name -> Type where
NameBinding : (elabAs : Term vars) -> (expTy : Term vars) ->
NameBinding : RigCount -> (elabAs : Term vars) -> (expTy : Term vars) ->
ImplBinding vars
AsBinding : (elabAs : Term vars) -> (expTy : Term vars) ->
AsBinding : RigCount -> (elabAs : Term vars) -> (expTy : Term vars) ->
(pat : Term vars) ->
ImplBinding vars
export
Show (ImplBinding vars) where
show (NameBinding p ty) = show (p, ty)
show (AsBinding p ty tm) = show (p, ty) ++ "@" ++ show tm
show (NameBinding c p ty) = show (p, ty)
show (AsBinding c p ty tm) = show (p, ty) ++ "@" ++ show tm
export
bindingMetas : ImplBinding vars -> NameMap ()
bindingMetas (NameBinding tm ty) = getMetas ty
bindingMetas (AsBinding tm ty pat)
bindingMetas (NameBinding c tm ty) = getMetas ty
bindingMetas (AsBinding c tm ty pat)
= insertAll (toList (getMetas ty)) (getMetas pat)
where
insertAll : List (Name, ()) -> NameMap () -> NameMap ()
@ -59,15 +59,20 @@ bindingMetas (AsBinding tm ty pat)
-- Get the type of an implicit name binding
export
bindingType : ImplBinding vars -> Term vars
bindingType (NameBinding _ ty) = ty
bindingType (AsBinding _ ty _) = ty
bindingType (NameBinding _ _ ty) = ty
bindingType (AsBinding _ _ ty _) = ty
-- Get the term (that is, the expanded thing it elaborates to, of the name
-- applied to the context) from an implicit binding
export
bindingTerm : ImplBinding vars -> Term vars
bindingTerm (NameBinding tm _) = tm
bindingTerm (AsBinding tm _ _) = tm
bindingTerm (NameBinding _ tm _) = tm
bindingTerm (AsBinding _ tm _ _) = tm
export
bindingRig : ImplBinding vars -> RigCount
bindingRig (NameBinding c _ _) = c
bindingRig (AsBinding c _ _ _) = c
-- Current elaboration state (preserved/updated throughout elaboration)
public export
@ -129,9 +134,9 @@ weakenedEState {e}
where
wknTms : (Name, ImplBinding vs) ->
(Name, ImplBinding (n :: vs))
wknTms (f, NameBinding x y) = (f, NameBinding (weaken x) (weaken y))
wknTms (f, AsBinding x y z)
= (f, AsBinding (weaken x) (weaken y) (weaken z))
wknTms (f, NameBinding c x y) = (f, NameBinding c (weaken x) (weaken y))
wknTms (f, AsBinding c x y z)
= (f, AsBinding c (weaken x) (weaken y) (weaken z))
strengthenedEState : Ref Ctxt Defs ->
Ref EST (EState (n :: vars)) ->
@ -160,22 +165,22 @@ strengthenedEState {n} {vars} c e fc env
strTms : Defs -> (Name, ImplBinding (n :: vars)) ->
Core (Name, ImplBinding vars)
strTms defs (f, NameBinding x y)
strTms defs (f, NameBinding c x y)
= do xnf <- normaliseHoles defs env x
ynf <- normaliseHoles defs env y
case (shrinkTerm xnf (DropCons SubRefl),
shrinkTerm ynf (DropCons SubRefl)) of
(Just x', Just y') => pure (f, NameBinding x' y')
(Just x', Just y') => pure (f, NameBinding c x' y')
_ => throw (GenericMsg fc ("Invalid unbound implicit " ++
show f ++ " " ++ show xnf ++ " : " ++ show ynf))
strTms defs (f, AsBinding x y z)
strTms defs (f, AsBinding c x y z)
= do xnf <- normaliseHoles defs env x
ynf <- normaliseHoles defs env y
znf <- normaliseHoles defs env y
case (shrinkTerm xnf (DropCons SubRefl),
shrinkTerm ynf (DropCons SubRefl),
shrinkTerm znf (DropCons SubRefl)) of
(Just x', Just y', Just z') => pure (f, AsBinding x' y' z')
(Just x', Just y', Just z') => pure (f, AsBinding c x' y' z')
_ => throw (GenericMsg fc ("Invalid as binding " ++
show f ++ " " ++ show xnf ++ " : " ++ show ynf))

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

@ -25,14 +25,11 @@ checkHole : {vars : _} ->
checkHole rig elabinfo nest env fc n_in (Just gexpty)
= do nm <- inCurrentNS (UN n_in)
expty <- getTerm gexpty
let env' = letToLam env -- we want all the names to appear in the
-- hole type
metaval <- metaVar fc rig env' nm expty
metaval <- metaVar fc rig env nm expty
pure (metaval, gexpty)
checkHole rig elabinfo nest env fc n_in exp
= do nmty <- genName "holeTy"
ty <- metaVar fc Rig0 env nmty (TType fc)
nm <- inCurrentNS (UN n_in)
let env' = letToLam env
metaval <- metaVar fc rig env' nm ty
metaval <- metaVar fc rig env nm ty
pure (metaval, gnf env ty)

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

@ -153,7 +153,7 @@ bindUnsolved {vars} fc elabmode _
do impn <- genVarName (nameRoot n)
tm <- metaVar fc rig env impn exp'
est <- get EST
put EST (record { toBind $= ((impn, NameBinding
put EST (record { toBind $= ((impn, NameBinding rig
(embedSub subvars tm)
(embedSub subvars exp')) ::) } est)
pure (embedSub sub tm)
@ -256,7 +256,7 @@ bindImplVars {vars} fc mode gam env imps_in scope scty
Bounds new -> (tm : Term vs) -> (ty : Term vs) ->
(Term (new ++ vs), Term (new ++ vs))
getBinds [] bs tm ty = (refsToLocals bs tm, refsToLocals bs ty)
getBinds ((n, metan, NameBinding _ bty) :: imps) bs tm ty
getBinds ((n, metan, NameBinding c _ bty) :: imps) bs tm ty
= let (tm', ty') = getBinds imps (Add n metan bs) tm ty
bty' = refsToLocals bs bty in
case mode of
@ -264,14 +264,14 @@ bindImplVars {vars} fc mode gam env imps_in scope scty
(Bind fc _ (Pi c Implicit bty') tm',
TType fc)
_ =>
(Bind fc _ (PVar RigW bty') tm',
Bind fc _ (PVTy RigW bty') ty')
getBinds ((n, metan, AsBinding _ bty bpat) :: imps) bs tm ty
(Bind fc _ (PVar c bty') tm',
Bind fc _ (PVTy c bty') ty')
getBinds ((n, metan, AsBinding c _ bty bpat) :: imps) bs tm ty
= let (tm', ty') = getBinds imps (Add n metan bs) tm ty
bty' = refsToLocals bs bty
bpat' = refsToLocals bs bpat in
(Bind fc _ (PLet RigW bpat' bty') tm',
Bind fc _ (PLet RigW bpat' bty') ty')
(Bind fc _ (PLet c bpat' bty') tm',
Bind fc _ (PLet c bpat' bty') ty')
normaliseHolesScope : Defs -> Env Term vars -> Term vars -> Core (Term vars)
normaliseHolesScope defs env (Bind fc n b sc)
@ -292,10 +292,10 @@ bindImplicits {vars} fc mode defs env hs tm ty
pure $ liftImps mode $ bindImplVars fc mode defs env hs' tm ty
where
nHoles : (Name, ImplBinding vars) -> Core (Name, ImplBinding vars)
nHoles (n, NameBinding tm ty)
= pure (n, NameBinding tm !(normaliseHolesScope defs env ty))
nHoles (n, AsBinding tm ty pat)
= pure (n, AsBinding tm !(normaliseHolesScope defs env ty) pat)
nHoles (n, NameBinding c tm ty)
= pure (n, NameBinding c tm !(normaliseHolesScope defs env ty))
nHoles (n, AsBinding c tm ty pat)
= pure (n, AsBinding c tm !(normaliseHolesScope defs env ty) pat)
export
implicitBind : {auto c : Ref Ctxt Defs} ->
@ -344,11 +344,11 @@ getToBind {vars} fc elabmode impmode env excepts toptm
pure res'
where
normBindingTy : Defs -> ImplBinding vars -> Core (ImplBinding vars)
normBindingTy defs (NameBinding tm ty)
= pure $ NameBinding tm !(normaliseHoles defs env ty)
normBindingTy defs (AsBinding tm ty pat)
= pure $ AsBinding tm !(normaliseHoles defs env ty)
!(normaliseHoles defs env pat)
normBindingTy defs (NameBinding c tm ty)
= pure $ NameBinding c tm !(normaliseHoles defs env ty)
normBindingTy defs (AsBinding c tm ty pat)
= pure $ AsBinding c tm !(normaliseHoles defs env ty)
!(normaliseHoles defs env pat)
normImps : Defs -> List Name -> List (Name, ImplBinding vars) ->
Core (List (Name, ImplBinding vars))
@ -428,20 +428,45 @@ checkBindVar rig elabinfo nest env fc str topexp
do (tm, exp, bty) <- mkPatternHole fc rig n env
(implicitMode elabinfo)
topexp
log 5 $ "Added Bound implicit " ++ show (n, (tm, exp, bty))
log 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
defs <- get Ctxt
est <- get EST
put EST
(record { boundNames $= ((n, NameBinding tm exp) ::),
toBind $= ((n, NameBinding tm bty) :: ) } est)
(record { boundNames $= ((n, NameBinding rig tm exp) ::),
toBind $= ((n, NameBinding rig tm bty) :: ) } est)
-- addNameType loc (UN str) env exp
checkExp rig elabinfo env fc tm (gnf env exp) topexp
Just bty =>
do -- TODO: for metadata addNameType loc (UN str) env ty
-- Check rig is consistent with the one in bty, and
-- update if necessary
combine n rig (bindingRig bty)
let tm = bindingTerm bty
let ty = bindingType bty
defs <- get Ctxt
checkExp rig elabinfo env fc tm (gnf env ty) topexp
where
updateRig : Name -> RigCount -> List (Name, ImplBinding vars) ->
List (Name, ImplBinding vars)
updateRig n c [] = []
updateRig n c ((bn, r) :: bs)
= if n == bn
then case r of
NameBinding _ tm ty => (bn, NameBinding c tm ty) :: bs
AsBinding _ tm ty p => (bn, AsBinding c tm ty p) :: bs
else (bn, r) :: updateRig n c bs
combine : Name -> RigCount -> RigCount -> Core ()
combine n Rig1 Rig1 = throw (LinearUsed fc 2 n)
combine n Rig1 RigW = throw (LinearUsed fc 2 n)
combine n RigW Rig1 = throw (LinearUsed fc 2 n)
combine n RigW RigW = pure ()
combine n Rig0 c = pure ()
combine n c Rig0
-- It was 0, make it c
= do est <- get EST
put EST (record { boundNames $= updateRig n c,
toBind $= updateRig n c } est)
export
checkBindHere : {vars : _} ->

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

@ -131,8 +131,8 @@ checkTerm rig elabinfo nest env (IBindHere fc binder sc) exp
= checkBindHere rig elabinfo nest env fc binder sc exp
checkTerm rig elabinfo nest env (IBindVar fc n) exp
= checkBindVar rig elabinfo nest env fc n exp
checkTerm rig elabinfo nest env (IAs fc n_in tm) exp
= checkAs rig elabinfo nest env fc n_in tm exp
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))

2
src/TTImp/Parser.idr
View File

@ -123,7 +123,7 @@ mutual
symbol "@"
pat <- simpleExpr fname indents
end <- location
pure (IAs (MkFC fname start end) (UN x) pat)
pure (IAs (MkFC fname start end) UseRight (UN x) pat)
simpleExpr : FileName -> IndentInfo -> Rule RawImp
simpleExpr fname indents

4
src/TTImp/ProcessData.idr
View File

@ -85,7 +85,7 @@ processData eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
Nothing <- lookupCtxtExact n (gamma defs)
| Just gdef => throw (AlreadyDefined fc n)
(ty, _) <- elabTerm !(resolveName n) InType eopts nest env
(ty, _, _) <- elabTerm !(resolveName n) InType eopts nest env
(IBindHere fc (PI Rig0) ty_raw)
(Just (gType dfc))
let fullty = abstractEnvType dfc env ty
@ -103,7 +103,7 @@ processData eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
= do n <- inCurrentNS n_in
log 1 $ "Processing " ++ show n
defs <- get Ctxt
(ty, _) <- elabTerm !(resolveName n) InType eopts nest env
(ty, _, _) <- elabTerm !(resolveName n) InType eopts nest env
(IBindHere fc (PI Rig0) ty_raw)
(Just (gType dfc))
let fullty = abstractEnvType dfc env ty

30
src/TTImp/ProcessDef.idr
View File

@ -139,14 +139,14 @@ checkClause : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(mult : RigCount) -> (hashit : Bool) ->
Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
ImpClause -> Core (Maybe Clause)
ImpClause -> Core (Maybe (Clause, Clause))
checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
= throw (InternalError "impossible not implemented yet")
checkClause mult hashit n opts nest env (PatClause fc lhs_in rhs)
= do lhs <- lhsInCurrentNS nest lhs_in
log 5 $ "Checking " ++ show lhs
logEnv 5 "In env" env
(lhstm, lhstyg) <- elabTerm n (InLHS mult) opts nest env
(lhstm, _, lhstyg) <- elabTerm n (InLHS mult) opts nest env
(IBindHere fc PATTERN lhs) Nothing
logTerm 10 "Checked LHS term" lhstm
lhsty <- getTerm lhstyg
@ -170,10 +170,20 @@ checkClause mult hashit n opts nest env (PatClause fc lhs_in rhs)
(vars' ** (sub', env', nest', lhstm', lhsty')) <-
extendEnv env SubRefl nest lhstm_lin lhsty_lin
rhstm <- checkTermSub n InExpr opts nest' env' env sub' rhs (gnf env' lhsty')
(rhstm, rhserased) <- checkTermSub n InExpr opts nest' env' env sub' rhs (gnf env' lhsty')
logTerm 5 "RHS term" rhstm
pure (Just (MkClause env' lhstm' rhstm))
pure (Just (MkClause env' lhstm' rhstm,
MkClause env' lhstm' rhserased))
nameListEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
nameListEq [] [] = Just Refl
nameListEq (x :: xs) (y :: ys) with (nameEq x y)
nameListEq (x :: xs) (x :: ys) | (Just Refl) with (nameListEq xs ys)
nameListEq (x :: xs) (x :: xs) | (Just Refl) | Just Refl= Just Refl
nameListEq (x :: xs) (x :: ys) | (Just Refl) | Nothing = Nothing
nameListEq (x :: xs) (y :: ys) | Nothing = Nothing
nameListEq _ _ = Nothing
toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
toPats (MkClause {vars} env lhs rhs)
@ -198,10 +208,16 @@ processDef {vars} opts nest env fc n_in cs_in
else Rig1
nidx <- resolveName n
cs <- traverse (checkClause mult hashit nidx opts nest env) cs_in
let pats = map toPats (mapMaybe id cs)
let pats = map toPats (map fst (mapMaybe id cs))
(cargs ** tree_ct) <- getPMDef fc CompileTime n ty (mapMaybe id cs)
(cargs ** tree_ct) <- getPMDef fc CompileTime n ty
(map fst (mapMaybe id cs))
(rargs ** tree_rt) <- getPMDef fc CompileTime n ty
(map snd (mapMaybe id cs))
let Just Refl = nameListEq cargs rargs
| Nothing => throw (InternalError "WAT")
log 5 $ "Case tree for " ++ show n ++ ": " ++ show tree_ct
addDef n (record { definition = PMDef cargs tree_ct tree_ct pats } gdef)
addDef n (record { definition = PMDef cargs tree_ct tree_rt pats } gdef)
pure ()

7
src/TTImp/ProcessType.idr
View File

@ -24,7 +24,7 @@ processType eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
log 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw
idx <- resolveName n
(ty, _) <- elabTerm idx InType (HolesOkay :: eopts) nest env
(ty, _, _) <- elabTerm idx InType (HolesOkay :: eopts) nest env
(IBindHere fc (PI Rig0) ty_raw)
(Just (gType fc))
logTermNF 5 (show n) [] (abstractEnvType tfc env ty)
@ -32,6 +32,11 @@ processType eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
let def = None -- TODO: External definitions
addDef (Resolved idx) (newDef fc n rig (abstractEnvType tfc env ty) vis def)
-- Flag it as checked, because we're going to check the clauses
-- from the top level.
-- But, if it's a case block, it'll be checked as part of the top
-- level check so don't set the flag.
when (not (InCase `elem` eopts)) $ setLinearCheck idx True
-- TODO: Interface hash and saving
pure ()

55
src/TTImp/TTImp.idr
View File

@ -33,6 +33,11 @@ mutual
public export
data BindMode = PI RigCount | PATTERN | NONE
-- For as patterns matching linear arguments, select which side is
-- consumed
public export
data UseSide = UseLeft | UseRight
public export
data RawImp : Type where
IVar : FC -> Name -> RawImp
@ -61,7 +66,7 @@ mutual
-- A name which should be implicitly bound
IBindVar : FC -> String -> RawImp
-- An 'as' pattern, valid on the LHS of a clause only
IAs : FC -> Name -> RawImp -> RawImp
IAs : FC -> UseSide -> Name -> RawImp -> RawImp
-- A 'dot' pattern, i.e. one which must also have the given value
-- by unification
IMustUnify : FC -> (reason : String) -> RawImp -> RawImp
@ -120,7 +125,7 @@ mutual
show (IBindHere fc b sc)
= "(%bindhere " ++ show sc ++ ")"
show (IBindVar fc n) = "$" ++ n
show (IAs fc n tm) = show n ++ "@(" ++ show tm ++ ")"
show (IAs fc _ n tm) = show n ++ "@(" ++ show tm ++ ")"
show (IMustUnify fc r tm) = ".(" ++ show tm ++ ")"
show (IPrimVal fc c) = show c
show (IHole _ x) = "?" ++ x
@ -244,31 +249,31 @@ lhsInCurrentNS nest (IVar loc n)
lhsInCurrentNS nest tm = pure tm
export
getAnnot : RawImp -> FC
getAnnot (IVar x _) = x
getAnnot (IPi x _ _ _ _ _) = x
getAnnot (ILam x _ _ _ _ _) = x
getAnnot (ILet x _ _ _ _ _) = x
getAnnot (ICase x _ _ _) = x
getAnnot (ILocal x _ _) = x
getAnnot (IUpdate x _ _) = x
getAnnot (IApp x _ _) = x
getAnnot (IImplicitApp x _ _ _) = x
getAnnot (ISearch x _) = x
getAnnot (IAlternative x _ _) = x
getAnnot (IRewrite x _ _) = x
getAnnot (ICoerced x _) = x
getAnnot (IPrimVal x _) = x
getAnnot (IHole x _) = x
getAnnot (IType x) = x
getAnnot (IBindVar x _) = x
getAnnot (IBindHere x _ _) = x
getAnnot (IMustUnify x _ _) = x
getAnnot (IAs x _ _) = x
getAnnot (Implicit x _) = x
getFC : RawImp -> FC
getFC (IVar x _) = x
getFC (IPi x _ _ _ _ _) = x
getFC (ILam x _ _ _ _ _) = x
getFC (ILet x _ _ _ _ _) = x
getFC (ICase x _ _ _) = x
getFC (ILocal x _ _) = x
getFC (IUpdate x _ _) = x
getFC (IApp x _ _) = x
getFC (IImplicitApp x _ _ _) = x
getFC (ISearch x _) = x
getFC (IAlternative x _ _) = x
getFC (IRewrite x _ _) = x
getFC (ICoerced x _) = x
getFC (IPrimVal x _) = x
getFC (IHole x _) = x
getFC (IType x) = x
getFC (IBindVar x _) = x
getFC (IBindHere x _ _) = x
getFC (IMustUnify x _ _) = x
getFC (IAs x _ _ _) = x
getFC (Implicit x _) = x
export
apply : RawImp -> List RawImp -> RawImp
apply f [] = f
apply f (x :: xs) = apply (IApp (getAnnot f) f x) xs
apply f (x :: xs) = apply (IApp (getFC f) f x) xs

2
src/TTImp/Unelab.idr
View File

@ -164,7 +164,7 @@ mutual
= do (p', _) <- unelabTy' umode env p
(tm', ty) <- unelabTy' umode env tm
case p' of
IVar _ n => pure (IAs fc n tm', ty)
IVar _ n => pure (IAs fc UseRight n tm', ty)
_ => pure (tm', ty) -- Should never happen!
unelabTy' umode env (TDelayed fc r tm)
= do (tm', ty) <- unelabTy' umode env tm

16
src/Yaffle/REPL.idr
View File

@ -31,13 +31,25 @@ process : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
ImpREPL -> Core Bool
process (Eval ttimp)
= do (tm, _) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing
= do (tm, _, _) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing
defs <- get Ctxt
tmnf <- normalise defs [] tm
coreLift (printLn !(unelab [] tmnf))
pure True
process (Check (IVar _ n))
= do defs <- get Ctxt
ns <- lookupTyName n (gamma defs)
traverse printName ns
pure True
where
printName : (Name, Int, ClosedTerm) -> Core ()
printName (n, _, tyh)
= do defs <- get Ctxt
ty <- normaliseHoles defs [] tyh
coreLift $ putStrLn $ show n ++ " : " ++
show !(unelab [] ty)
process (Check ttimp)
= do (tm, gty) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing
= do (tm, _, gty) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing
defs <- get Ctxt
tyh <- getTerm gty
ty <- normaliseHoles defs [] tyh

3
tests/Main.idr
View File

@ -10,7 +10,8 @@ ttimpTests
"basic006", "basic007",
"eta001", "eta002",
"nest001", "nest002",
"perf001", "perf002", "perf003"]
"perf001", "perf002", "perf003",
"qtt001", "qtt002"]
chdir : String -> IO Bool
chdir dir

4
tests/ttimp/basic003/Auto.yaff
View File

@ -13,10 +13,10 @@ data Elem : $a -> List $a -> Type where
data Pair : Type -> Type -> Type where
MkPair : $a -> $b -> Pair $a $b
fst : Pair $a $b -> $a
fst : {0 a, b : _} -> Pair a b -> a
fst (MkPair $x _) = x
snd : Pair $a $b -> $b
snd : {0 a, b : _} -> Pair a b -> b
snd (MkPair _ $y) = y
%pair Pair fst snd

2
tests/ttimp/basic007/Hole.yaff
View File

@ -12,4 +12,4 @@ plus (S $k) $y = S (plus k y)
append : Vect $n $a -> Vect $m $a -> Vect (plus $n $m) $a
append Nil $ys = ys
append (Cons $x $xs) $ys = Cons $x ?foo
append (Cons $x $xs) $ys = Cons x ?foo

6
tests/ttimp/basic007/expected
View File

@ -1,11 +1,11 @@
Processing as TTImp
Written TTC
Yaffle> (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
Yaffle> Bye for now!
Processing as TTC
Read 2 holes
Read 1 holes
Read 0 guesses
Read 0 constraints
Read TTC
Yaffle> (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
Yaffle> Bye for now!

2
tests/ttimp/eta001/expected
View File

@ -1,5 +1,5 @@
Processing as TTImp
Written TTC
Yaffle> ((Main.Refl [Just {b:15} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
Yaffle> ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
Yaffle> Bye for now!

2
tests/ttimp/eta002/expected
View File

@ -1,4 +1,4 @@
Processing as TTImp
Eta.yaff:16:10--17:1:When unifying: ($resolved84 ?Main.{{b:15}:25}_[] ?Main.{{b:15}:25}_[] ?Main.{x:26}_[] ?Main.{x:26}_[]) and ($resolved84 (x : Char) -> (y : ?Main.{_:20}_[x[0]]) -> $resolved92 ({arg:16} : Integer) -> ({arg:17} : Integer) -> $resolved92 $resolved93 \x : Char => \y : ?Main.{_:20}_[x[0]] => ($resolved93 ?Main.{_:24}_[x[1], y[0]] ?Main.{_:23}_[x[1], y[0]]))
Eta.yaff:16:10--17:1:When unifying: ($resolved84 ?Main.{{b:15}:25}_[] ?Main.{{b:15}:25}_[] ?Main.{x:26}_[] ?Main.{x:26}_[]) and ($resolved84 ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) (({arg:16} : Integer) -> (({arg:17} : Integer) -> $resolved92)) $resolved93 \x : Char => \y : ?Main.{_:20}_[x[0]] => ($resolved93 ?Main.{_:24}_[x[1], y[0]] ?Main.{_:23}_[x[1], y[0]]))
Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
Yaffle> Bye for now!

2
tests/ttimp/perf002/expected
View File

@ -1,4 +1,4 @@
Processing as TTImp
Written TTC
Yaffle> ((Main.Vect (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Main.Bool)
Yaffle> Main.stuff : ((Main.Vect (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Main.Bool)
Yaffle> Bye for now!

2
tests/ttimp/perf003/expected
View File

@ -1,5 +1,5 @@
Processing as TTImp
Written TTC
Yaffle> Integer
Yaffle> Main.idInt : Integer
Yaffle> 94
Yaffle> Bye for now!

15
tests/ttimp/qtt001/QTT.yaff Normal file
View File

@ -0,0 +1,15 @@
data Pair : Type -> Type -> Type where
MkPair : (1 xa : $a) -> (1 ya : $b) -> Pair $a $b
dup : (1 x : $a) -> Pair $a $a
dup $x = MkPair ?foo ?bar
dup1 : (1 x : $a) -> Pair $a $a
dup1 $x = MkPair x ?baz1
dup2 : (1 x : $a) -> Pair $a $a
dup2 $x = MkPair ?baz2 x
dupbad : (1 x : $a) -> Pair $a $a
dupbad $x = MkPair x x

7
tests/ttimp/qtt001/expected Normal file
View File

@ -0,0 +1,7 @@
Processing as TTImp
QTT.yaff:14:13--16:1:There are 2 uses of linear name x
Yaffle> Main.foo : (%pi Rig0 Explicit Just {a:4} %type (%pi Rig1 Explicit Just x {a:4} {a:4}))
Yaffle> Main.bar : (%pi Rig0 Explicit Just {a:4} %type (%pi Rig1 Explicit Just x {a:4} {a:4}))
Yaffle> Main.baz1 : (%pi Rig0 Explicit Just {a:11} %type (%pi Rig0 Explicit Just x {a:11} {a:11}))
Yaffle> Main.baz2 : (%pi Rig0 Explicit Just {a:18} %type (%pi Rig0 Explicit Just x {a:18} {a:18}))
Yaffle> Bye for now!

5
tests/ttimp/qtt001/input Normal file
View File

@ -0,0 +1,5 @@
:t foo
:t bar
:t baz1
:t baz2
:q

3
tests/ttimp/qtt001/run Executable file
View File

@ -0,0 +1,3 @@
$1 QTT.yaff < input
rm -rf build

26
tests/ttimp/qtt002/QTT.yaff Normal file
View File

@ -0,0 +1,26 @@
data Nat : Type where
Z : Nat
S : Nat -> Nat
plus : Nat -> Nat -> Nat
plus Z $y = y
plus (S $k) $y = S (plus k y)
data Vect : Nat -> Type -> Type where
Nil : Vect Z $a
Cons : $a -> (1 xs : Vect $k $a) -> Vect (S $k) $a
append : (1 xs : Vect $n $a) -> Vect $m $a -> Vect (plus $n $m) $a
append (Cons $x zs@(Cons $y $ws)) $ys = ?foo -- zs usable, y+ws not
cappend : (1 xs : Vect $n $a) -> Vect $m $a -> Vect (plus $n $m) $a
cappend $xs $ys
= case xs of
Nil => ys
Cons $x $zs => ?bar -- zs usable, xs not
cappend2 : (1 xs : Vect $n $a) -> Vect $m $a -> Vect (plus $n $m) $a
cappend2 $xs $ys
= case xs of
Nil => ys
Cons $x $zs => let ts = zs in ?baz -- ts usable, xs+zs not

6
tests/ttimp/qtt002/expected Normal file
View File

@ -0,0 +1,6 @@
Processing as TTImp
Written TTC
Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:33} Main.Nat (%pi Rig0 Explicit Just {a:32} %type (%pi Rig0 Explicit Just {k:31} Main.Nat (%pi RigW Explicit Nothing {a:32} (%pi Rig0 Explicit Just y {a:32} (%pi Rig0 Explicit Just ws ((Main.Vect {k:31}) {a:32}) (%let Rig1 zs ((Main.Vect (Main.S {k:31})) {a:32}) ((((Main.Cons [Just k = {k:31}]) [Just a = {a:32}]) y) ws) (%pi RigW Explicit Nothing ((Main.Vect {m:33}) {a:32}) ((Main.Vect ((Main.plus (Main.S (Main.S {k:31}))) {m:33})) {a:32})))))))))
Yaffle> Main.bar : (%pi Rig0 Explicit Just {m:44} Main.Nat (%pi Rig0 Explicit Just {a:43} %type (%pi Rig0 Explicit Just {n:42} Main.Nat (%pi Rig0 Explicit Just xs ((Main.Vect {n:42}) {a:43}) (%pi RigW Explicit Nothing ((Main.Vect {m:44}) {a:43}) (%pi Rig0 Explicit Just {_:75} %type (%pi Rig0 Explicit Just {_:74} Main.Nat (%pi RigW Explicit Just {_:77} ((Main.Vect {_:74}) {_:75}) (%pi Rig0 Explicit Just {k:76} Main.Nat (%pi RigW Explicit Just x {_:75} (%pi Rig1 Explicit Just zs ((Main.Vect {k:76}) {_:75}) (%let Rig0 xs ((Main.Vect (Main.S {k:76})) {_:75}) ((((Main.Cons [Just k = {k:76}]) [Just a = {_:75}]) x) zs) (%let RigW ys ((Main.Vect {_:74}) {_:75}) {_:77} ((Main.Vect ((Main.plus (Main.S {k:76})) {_:74})) {_:75}))))))))))))))
Yaffle> Main.baz : (%pi Rig0 Explicit Just {m:88} Main.Nat (%pi Rig0 Explicit Just {a:87} %type (%pi Rig0 Explicit Just {n:86} Main.Nat (%pi Rig0 Explicit Just xs ((Main.Vect {n:86}) {a:87}) (%pi RigW Explicit Nothing ((Main.Vect {m:88}) {a:87}) (%pi Rig0 Explicit Just {_:119} %type (%pi Rig0 Explicit Just {_:118} Main.Nat (%pi RigW Explicit Just {_:121} ((Main.Vect {_:118}) {_:119}) (%pi Rig0 Explicit Just {k:120} Main.Nat (%pi RigW Explicit Just x {_:119} (%pi Rig0 Explicit Just zs ((Main.Vect {k:120}) {_:119}) (%let Rig0 xs ((Main.Vect (Main.S {k:120})) {_:119}) ((((Main.Cons [Just k = {k:120}]) [Just a = {_:119}]) x) zs) (%let RigW ys ((Main.Vect {_:118}) {_:119}) {_:121} (%let Rig1 ts ((Main.Vect {k:120}) {_:119}) zs ((Main.Vect ((Main.plus (Main.S {k:120})) {_:118})) {_:119})))))))))))))))
Yaffle> Bye for now!

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

@ -0,0 +1,4 @@
:t foo
:t bar
:t baz
:q

3
tests/ttimp/qtt002/run Executable file
View File

@ -0,0 +1,3 @@
$1 QTT.yaff < input
rm -rf build

1
yaffle.ipkg
View File

@ -14,6 +14,7 @@ modules =
Core.FC,
Core.GetType,
Core.Hash,
Core.LinearCheck,
Core.Name,
Core.Normalise,
Core.Options,