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

Basic TTC saving and loading now works

Browse Source 
Only save the parts of terms and definitions which are needed for
typechecking and evaluation (so, for example, we don't need types for
machine generated metavariables, don't need types on lambdas, etc).
This commit is contained in:
Edwin Brady 2019-04-25 14:46:36 +01:00
parent a48d90f821
commit 762f6010dd
20 changed files with 430 additions and 334 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
sample/Interp.yaff
View File

@ -71,4 +71,3 @@ testAdd = Lam (Lam (Op plus (Var Stop) (Var (Pop Stop))))
main : Nat
main = interp ENil testAdd (S (S Z)) (S (S Z))

12
src/Core/Binary.idr
View File

@ -117,18 +117,17 @@ readTTCFile modns as r b
importHashes <- fromBuf r b
-- Read in name map, update 'r'
r <- readNameMap r b
coreLift $ putStrLn "Read name map"
defs <- get Ctxt
gam' <- updateEntries (gamma defs) modns as 0 (max r) r
setCtxt gam'
holes <- fromBuf r b
coreLift $ putStrLn $ "Read " ++ show (length holes) ++ " holes"
coreLift $ putStrLn $ "Read " ++ show holes ++ " holes"
guesses <- fromBuf r b
coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ "guesses"
coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ " guesses"
constraints <- the (Core (List (Int, Constraint))) $ fromBuf r b
coreLift $ putStrLn $ "Read " ++ show (length constraints) ++ "constraints"
coreLift $ putStrLn $ "Read " ++ show (length constraints) ++ " constraints"
defs <- fromBuf r b
coreLift $ putStrLn ("Read defs of " ++ show (map fullname defs))
-- coreLift $ putStrLn $ "Read " ++ show (length (map fullname defs)) ++ " defs"
imp <- fromBuf r b
cns <- fromBuf r b
ex <- fromBuf r b
@ -154,7 +153,7 @@ writeToTTC extradata fname
= do buf <- initBinary
defs <- get Ctxt
ust <- get UST
gdefs <- getSaveDefs (getSave defs) [] defs
gdefs <- getSaveDefs !getSave [] defs
log 5 $ "Writing " ++ fname ++ " with hash " ++ show (ifaceHash defs)
r <- getNameRefs (gamma defs)
writeTTCFile buf
@ -211,6 +210,7 @@ readFromTTC loc reexp fname modNS importAs
ttc <- readTTCFile modNS as r bin
traverse (addGlobalDef modNS as) (context ttc)
setNS (currentNS ttc)
resetFirstEntry
-- Finally, update the unification state with the holes from the
-- ttc

29
src/Core/CaseBuilder.idr
View File

@ -113,11 +113,13 @@ substInPats fc n tm (p :: ps)
= do (p', ps') <- substInPatInfo fc n tm p ps
pure (p' :: !(substInPats fc n tm ps'))
getPat : IsVar name idx ps -> NamedPats ns ps -> PatInfo name ns
getPat : {idx : Nat} ->
.(IsVar name idx ps) -> NamedPats ns ps -> PatInfo name ns
getPat First (x :: xs) = x
getPat (Later p) (x :: xs) = getPat p xs
dropPat : (el : IsVar name idx ps) ->
dropPat : {idx : Nat} ->
.(el : IsVar name idx ps) ->
NamedPats ns ps -> NamedPats ns (dropVar ps el)
dropPat First (x :: xs) = xs
dropPat (Later p) (x :: xs) = x :: dropPat p xs
@ -454,7 +456,7 @@ groupCons fc fn pvars cs
= do gs' <- addConstG c pats rhs gs
pure (g :: gs')
addGroup : Pat -> IsVar name idx vars ->
addGroup : {idx : Nat} -> Pat -> .(IsVar name idx vars) ->
NamedPats vars todo -> Term vars ->
List (Group vars todo) ->
Core (List (Group vars todo))
@ -583,12 +585,12 @@ countDiff xs = length (distinct [] (map getFirstCon xs))
getScore : {auto i : Ref PName Int} ->
{auto c : Ref Ctxt Defs} ->
FC -> Name -> IsVar name idx (p :: ps) ->
FC -> Name ->
List (NamedPats ns (p :: ps)) ->
Core (Either CaseError (IsVar name idx (p :: ps), Nat))
getScore fc name prf npss
Core (Either CaseError ())
getScore fc name npss
= do catch (do sameType fc name (mkEnv fc ns) npss
pure (Right (prf, countDiff npss)))
pure (Right ()))
(\err => case err of
CaseCompile _ _ err => pure (Left err)
_ => throw err)
@ -602,9 +604,9 @@ pickNext : {auto i : Ref PName Int} ->
pickNext {ps = []} fc fn npss
= if samePat npss
then pure (MkVar First)
else do Right (p, sc) <- getScore fc fn First npss
else do Right () <- getScore fc fn npss
| Left err => throw (CaseCompile fc fn err)
pure (MkVar p)
pure (MkVar First)
pickNext {ps = q :: qs} fc fn npss
= if samePat npss
then pure (MkVar First)
@ -612,11 +614,11 @@ pickNext {ps = q :: qs} fc fn npss
do (MkVar var) <- pickNext fc fn (map tail npss)
pure (MkVar (Later var))
moveFirst : (el : IsVar name idx ps) -> NamedPats ns ps ->
moveFirst : {idx : Nat} -> .(el : IsVar name idx ps) -> NamedPats ns ps ->
NamedPats ns (name :: dropVar ps el)
moveFirst el nps = getPat el nps :: dropPat el nps
shuffleVars : (el : IsVar name idx todo) -> PatClause vars todo ->
shuffleVars : {idx : Nat} -> .(el : IsVar name idx todo) -> PatClause vars todo ->
PatClause vars (name :: dropVar todo el)
shuffleVars el (MkPatClause pvars lhs rhs) = MkPatClause pvars (moveFirst el lhs) rhs
@ -651,7 +653,7 @@ mutual
caseGroups : {auto i : Ref PName Int} ->
{auto c : Ref Ctxt Defs} ->
FC -> Name -> Phase ->
IsVar pvar idx vars -> Term vars ->
{idx : Nat} -> .(IsVar pvar idx vars) -> Term vars ->
List (Group vars todo) -> Maybe (CaseTree vars) ->
Core (CaseTree vars)
caseGroups {vars} fc fn phase el ty gs errorCase
@ -810,7 +812,8 @@ simpleCase : {auto c : Ref Ctxt Defs} ->
(clauses : List (ClosedTerm, ClosedTerm)) ->
Core (args ** CaseTree args)
simpleCase fc phase fn ty def clauses
= do ps <- traverse (toPatClause fc fn) clauses
= do log 5 $ "Compiling clauses " ++ show clauses
ps <- traverse (toPatClause fc fn) clauses
defs <- get Ctxt
patCompile fc fn phase ty ps def

22
src/Core/CaseTree.idr
View File

@ -2,6 +2,8 @@ module Core.CaseTree
import Core.TT
%default covering
mutual
public export
data CaseTree : List Name -> Type where
@ -65,7 +67,7 @@ mutual
insertCaseNames : (ns : List Name) -> CaseTree (outer ++ inner) ->
CaseTree (outer ++ (ns ++ inner))
insertCaseNames {inner} {outer} ns (Case idx prf scTy alts)
= let (_ ** prf') = insertVarNames {outer} {inner} {ns} _ prf in
= let MkVar prf' = insertVarNames {outer} {inner} {ns} _ prf in
Case _ prf' (insertNames {outer} ns scTy)
(map (insertCaseAltNames {outer} {inner} ns) alts)
insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x)
@ -89,7 +91,7 @@ mutual
export
thinTree : (n : Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ n :: inner)
thinTree n (Case idx prf scTy alts)
= let (_ ** prf') = insertVar {n} _ prf in
= let MkVar prf' = insertVar {n} _ prf in
Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
thinTree n (STerm tm) = STerm (thin n tm)
thinTree n (Unmatched msg) = Unmatched msg
@ -99,24 +101,26 @@ export
Weaken CaseTree where
weakenNs ns t = insertCaseNames {outer = []} ns t
export
mkPat' : List Pat -> ClosedTerm -> ClosedTerm -> Pat
mkPat' [] orig (Ref fc Bound n) = PLoc fc n
mkPat' args orig (Ref fc Bound n) = PLoc fc n
mkPat' args orig (Ref fc (DataCon t a) n) = PCon fc n t a args
mkPat' args orig (Ref fc (TyCon t a) n) = PTyCon fc n a args
mkPat' [] orig (Bind fc x (Pi _ _ s) t)
mkPat' args orig (Bind fc x (Pi _ _ s) t)
= let t' = subst (Erased fc) t in
PArrow fc x (mkPat' [] s s) (mkPat' [] t' t')
mkPat' args orig (App fc fn p arg)
= let parg = mkPat' [] arg arg in
mkPat' (parg :: args) orig fn
mkPat' [] orig (As fc (Ref _ Bound n) ptm)
mkPat' (parg :: args) orig fn
mkPat' args orig (As fc (Ref _ Bound n) ptm)
= PAs fc n (mkPat' [] ptm ptm)
mkPat' [] orig (PrimVal fc c) = PConst fc c
mkPat' args orig (PrimVal fc c) = PConst fc c
mkPat' args orig tm = PUnmatchable (getLoc orig) orig
export
argToPat : ClosedTerm -> Pat
argToPat tm = mkPat' [] tm tm
argToPat tm
= mkPat' [] tm tm
export
mkTerm : (vars : List Name) -> Pat -> Term vars
@ -132,7 +136,7 @@ mkTerm vars (PArrow fc x s t)
= Bind fc x (Pi RigW Explicit (mkTerm vars s)) (mkTerm (x :: vars) t)
mkTerm vars (PLoc fc n)
= case isVar n vars of
Just (_ ** prf) => Local fc Nothing _ prf
Just (MkVar prf) => Local fc Nothing _ prf
_ => Ref fc Bound n
mkTerm vars (PUnmatchable fc tm) = embed tm

94
src/Core/Context.idr
View File

@ -23,6 +23,7 @@ data Arr : Type where
export
record Context a where
constructor MkContext
firstEntry : Int -- First entry in the current source file
nextEntry : Int
-- Map from full name to its position in the context
resolvedAs : NameMap Int
@ -64,7 +65,7 @@ initCtxtS : Int -> Core (Context a)
initCtxtS s
= do arr <- coreLift $ newArray s
aref <- newRef Arr arr
pure (MkContext 0 empty empty aref [])
pure (MkContext 0 0 empty empty aref [])
export
initCtxt : Core (Context a)
@ -92,18 +93,22 @@ getPosition n ctxt
do log 10 $ "Found " ++ show n ++ " " ++ show idx
pure (idx, ctxt)
Nothing =>
do let idx = nextEntry ctxt + 1
do let idx = nextEntry ctxt
let a = content ctxt
arr <- get Arr
when (idx >= max arr) $
do arr' <- coreLift $ newArrayCopy (max arr + Grow) arr
put Arr arr'
log 10 $ "Added " ++ show n ++ " " ++ show idx
pure (idx, record { nextEntry = idx,
pure (idx, record { nextEntry = idx + 1,
resolvedAs $= insert n idx,
possibles $= addPossible n idx
} ctxt)
export
getNameID : Name -> Context a -> Maybe Int
getNameID n ctxt = lookup n (resolvedAs ctxt)
-- Add the name to the context, or update the existing entry if it's already
-- there.
export
@ -344,21 +349,28 @@ record GlobalDef where
export
TTC GlobalDef where
toBuf b gdef
= do toBuf b (location gdef)
toBuf b (fullname gdef)
toBuf b (type gdef)
toBuf b (multiplicity gdef)
toBuf b (visibility gdef)
toBuf b (flags gdef)
-- Only write full details for user specified names. The others will
-- be holes where all we will ever need after loading is the definition
= do toBuf b (fullname gdef)
toBuf b (definition gdef)
when (isUserName (fullname gdef)) $
do toBuf b (location gdef)
toBuf b (type gdef)
toBuf b (multiplicity gdef)
toBuf b (visibility gdef)
toBuf b (flags gdef)
fromBuf r b
= do loc <- fromBuf r b; name <- fromBuf r b
coreLift $ putStrLn $ "Read " ++ show name
ty <- fromBuf r b; mul <- fromBuf r b
vis <- fromBuf r b; fl <- fromBuf r b
= do name <- fromBuf r b
def <- fromBuf r b
pure (MkGlobalDef loc name ty mul vis fl def)
if isUserName name
then do loc <- fromBuf r b;
ty <- fromBuf r b; mul <- fromBuf r b
vis <- fromBuf r b; fl <- fromBuf r b
pure (MkGlobalDef loc name ty mul vis fl def)
else do let fc = emptyFC
pure (MkGlobalDef fc name (Erased fc)
RigW Public [] def)
export
newDef : FC -> Name -> RigCount -> ClosedTerm -> Visibility -> Def -> GlobalDef
@ -394,18 +406,6 @@ initDefs
= do gam <- initCtxt
pure (MkDefs gam ["Main"] defaults empty 100 5381 [] [] [])
export
getSave : Defs -> List Name
getSave = map Basics.fst . toList . toSave
-- Note that the name should be saved when writing out a .ttc
export
addToSave : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
addToSave n
= do defs <- get Ctxt
put Ctxt (record { toSave $= insert n } defs)
-- Label for context references
export
data Ctxt : Type where
@ -437,6 +437,39 @@ setCtxt gam
= do defs <- get Ctxt
put Ctxt (record { gamma = gam } defs)
-- Get the names to save. These are the ones explicitly noted, and the
-- ones between firstEntry and nextEntry (which are the names introduced in
-- the current source file)
export
getSave : {auto c : Ref Ctxt Defs} -> Core (List Name)
getSave
= do defs <- get Ctxt
let gam = gamma defs
let ns = toSave defs
let a = content gam
arr <- get Arr
ns' <- coreLift $ addAll (firstEntry gam) (nextEntry gam) ns arr
pure (map fst (toList ns'))
where
addAll : Int -> Int -> NameMap () -> IOArray GlobalDef -> IO (NameMap ())
addAll first last ns arr
= if first == last
then pure ns
else do Just d <- readArray arr first
| Nothing => addAll (first + 1) last ns arr
case fullname d of
PV _ _ => addAll (first + 1) last ns arr
_ => addAll (first + 1) last
(insert (Resolved first) () ns) arr
-- Explicitly note that the name should be saved when writing out a .ttc
export
addToSave : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
addToSave n
= do defs <- get Ctxt
put Ctxt (record { toSave $= insert n () } defs)
-- Specific lookup functions
export
lookupDefExact : Name -> Context GlobalDef -> Core (Maybe Def)
@ -547,6 +580,15 @@ setNextEntry i
= do defs <- get Ctxt
put Ctxt (record { gamma->nextEntry = i } defs)
-- Set the 'first entry' index (i.e. the first entry in the current file)
-- to the place we currently are in the context
export
resetFirstEntry : {auto c : Ref Ctxt Defs} ->
Core ()
resetFirstEntry
= do defs <- get Ctxt
put Ctxt (record { gamma->firstEntry = nextEntry (gamma defs) } defs)
export
toFullNames : {auto c : Ref Ctxt Defs} ->
Term vars -> Core (Term vars)

44
src/Core/Env.idr
View File

@ -17,16 +17,21 @@ length : Env tm xs -> Nat
length [] = 0
length (x :: xs) = S (length xs)
public export
data IsDefined : Name -> List Name -> Type where
MkIsDefined : {idx : Nat} -> RigCount -> .(IsVar n idx vars) ->
IsDefined n vars
export
defined : {vars : _} ->
(n : Name) -> Env Term vars ->
Maybe (idx ** (RigCount, IsVar n idx vars))
Maybe (IsDefined n vars)
defined n [] = Nothing
defined {vars = x :: xs} n (b :: env)
= case nameEq n x of
Nothing => do (idx ** (rig, prf)) <- defined n env
pure (_ ** (rig, Later prf))
Just Refl => Just (_ ** (multiplicity b, First))
Nothing => do MkIsDefined rig prf <- defined n env
pure (MkIsDefined rig (Later prf))
Just Refl => Just (MkIsDefined (multiplicity b) First)
export
bindEnv : FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
@ -54,43 +59,26 @@ revNs (v :: vs) ns
-- in big environments
-- Also reversing the names at the end saves significant time over concatenating
-- when environments get fairly big.
export
getBinderUnder : Weaken tm =>
{idx : Nat} ->
(ns : List Name) ->
IsVar x idx vars -> Env tm vars ->
.(IsVar x idx vars) -> Env tm vars ->
Binder (tm (reverse ns ++ vars))
getBinderUnder {vars = v :: vs} ns First (b :: env)
getBinderUnder {idx = Z} {vars = v :: vs} ns First (b :: env)
= rewrite appendAssociative (reverse ns) [v] vs in
rewrite revNs [v] ns in
map (weakenNs (reverse (v :: ns))) b
getBinderUnder {vars = v :: vs} ns (Later lp) (b :: env)
getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env)
= rewrite appendAssociative (reverse ns) [v] vs in
rewrite revNs [v] ns in
getBinderUnder (v :: ns) lp env
export
getBinder : Weaken tm => IsVar x idx vars -> Env tm vars -> Binder (tm vars)
getBinder : Weaken tm =>
{idx : Nat} ->
.(IsVar x idx vars) -> Env tm vars -> Binder (tm vars)
getBinder el env = getBinderUnder [] el env
export
getLetBinderUnder : Weaken tm =>
(ns : List Name) ->
IsVar x idx vars -> Env tm vars ->
Maybe (tm (reverse ns ++ vars))
getLetBinderUnder {vars = v :: vs} ns First (Let mrig val ty :: env)
= rewrite appendAssociative (reverse ns) [v] vs in
rewrite revNs [v] ns in
Just (weakenNs (reverse (v :: ns)) val)
getLetBinderUnder ns First _ = Nothing
getLetBinderUnder {vars = v :: vs} ns (Later lp) (b :: env)
= rewrite appendAssociative (reverse ns) [v] vs in
rewrite revNs [v] ns in
getLetBinderUnder (v :: ns) lp env
export
getLetBinder : Weaken tm => IsVar x idx vars -> Env tm vars -> Maybe (tm vars)
getLetBinder el env = getLetBinderUnder [] el env
-- Make a type which abstracts over an environment
-- Don't include 'let' bindings, since they have a concrete value and
-- shouldn't be generalised

32
src/Core/Normalise.idr
View File

@ -78,13 +78,13 @@ parameters (defs : Defs, opts : EvalOpts)
evalLocal : {vars : _} ->
Env Term free -> LocalEnv free vars ->
FC -> Maybe RigCount ->
(idx : Nat) -> IsVar name idx (vars ++ free) ->
(idx : Nat) -> .(IsVar name idx (vars ++ free)) ->
Stack free ->
Core (NF free)
evalLocal {vars = []} env locs fc mrig idx prf stk
= case getLetBinder prf env of
Nothing => pure $ NApp fc (NLocal mrig idx prf) stk
Just val => eval env [] val stk
= case getBinder prf env of
Let _ val _ => eval env [] val stk
_ => pure $ NApp fc (NLocal mrig idx prf) stk
evalLocal env (MkClosure opts locs' env' tm' :: locs) fc mrig Z First stk
= evalWithOpts defs opts env' locs' tm' stk
evalLocal {free} {vars = x :: xs}
@ -99,8 +99,8 @@ parameters (defs : Defs, opts : EvalOpts)
= evalRef {vars = xs} env locs False fc nt fn (args ++ stk)
(NApp fc (NRef nt fn) args)
applyToStack (NApp fc (NLocal mrig idx p) args) stk
= let (idx' ** p') = insertVarNames {outer=[]} {ns = xs} idx p in
evalLocal env locs fc mrig idx' p' (args ++ stk)
= let MkVar p' = insertVarNames {outer=[]} {ns = xs} idx p in
evalLocal env locs fc mrig _ p' (args ++ stk)
applyToStack (NDCon fc n t a args) stk
= pure $ NDCon fc n t a (args ++ stk)
applyToStack (NTCon fc n t a args) stk
@ -324,28 +324,28 @@ mutual
FC -> Bounds bound -> Env Term free -> NHead free ->
Core (Term (bound ++ free))
quoteHead {bound} q defs fc bounds env (NLocal mrig _ prf)
= let (_ ** prf') = addLater bound prf in
= let MkVar prf' = addLater bound prf in
pure $ Local fc mrig _ prf'
where
addLater : (ys : List Name) -> IsVar n idx xs ->
(idx' ** IsVar n idx' (ys ++ xs))
addLater [] isv = (_ ** isv)
Var (ys ++ xs)
addLater [] isv = MkVar isv
addLater (x :: xs) isv
= let (_ ** isv') = addLater xs isv in
(_ ** Later isv')
= let MkVar isv' = addLater xs isv in
MkVar (Later isv')
quoteHead q defs fc bounds env (NRef Bound n)
= case findName bounds of
Just (_ ** _ ** p) => pure $ Local fc Nothing _ (varExtend p)
Just (MkVar p) => pure $ Local fc Nothing _ (varExtend p)
Nothing => pure $ Ref fc Bound n
where
findName : Bounds bound' -> Maybe (x ** idx ** IsVar x idx bound')
findName : Bounds bound' -> Maybe (Var bound')
findName None = Nothing
findName (Add x n' ns)
= case nameEq n n' of
Just Refl => Just (_ ** _ ** First)
Just Refl => Just (MkVar First)
Nothing =>
do (_ ** _ ** p) <- findName ns
Just (_ ** _ ** Later p)
do (MkVar p) <- findName ns
Just (MkVar (Later p))
quoteHead q defs fc bounds env (NRef nt n) = pure $ Ref fc nt n
quoteHead q defs fc bounds env (NMeta n i args)
= do args' <- quoteArgs q defs bounds env args

143
src/Core/TT.idr
View File

@ -245,13 +245,13 @@ data IsVar : Name -> Nat -> List Name -> Type where
Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
public export
dropVar : (ns : List Name) -> IsVar name idx ns -> List Name
dropVar : (ns : List Name) -> {idx : Nat} -> .(IsVar name idx ns) -> List Name
dropVar (n :: xs) First = xs
dropVar (n :: xs) (Later p) = n :: dropVar xs p
public export
data Var : List Name -> Type where
MkVar : {i : Nat} -> {n : _} -> IsVar n i vars -> Var vars
MkVar : {i : Nat} -> {n : _} -> .(IsVar n i vars) -> Var vars
export
sameVar : {i, j : _} -> IsVar n i xs -> IsVar m j xs -> Bool
@ -263,6 +263,10 @@ record AppInfo where
argname : Maybe Name
plicit : PiInfo
export
Show AppInfo where
show ap = "AppInfo: " ++ show (argname ap, plicit ap)
export
appInf : Maybe Name -> PiInfo -> AppInfo
appInf n p = MkAppInfo n p
@ -292,7 +296,7 @@ public export
data Term : List Name -> Type where
Local : {name : _} ->
FC -> Maybe RigCount ->
(idx : Nat) -> IsVar name idx vars -> Term vars
(idx : Nat) -> .(IsVar name idx vars) -> Term vars
Ref : FC -> NameType -> (name : Name) -> Term vars
-- Metavariables and the scope they are applied to
Meta : FC -> Name -> Int -> List (Term vars) -> Term vars
@ -419,39 +423,39 @@ interface Weaken (tm : List Name -> Type) where
export
insertVar : {outer : _} ->
(idx : _) ->
IsVar name idx (outer ++ inner) ->
(idx' ** IsVar name idx' (outer ++ n :: inner))
insertVar {outer = []} idx x = (_ ** Later x)
insertVar {outer = (name :: xs)} Z First = (_ ** First)
(idx : Nat) ->
.(IsVar name idx (outer ++ inner)) ->
Var (outer ++ n :: inner)
insertVar {outer = []} idx x = MkVar (Later x)
insertVar {outer = (name :: xs)} Z First = MkVar First
insertVar {n} {outer = (x :: xs)} (S i) (Later y)
= let (_ ** prf) = insertVar {n} i y in
(_ ** Later prf)
= let MkVar prf = insertVar {n} i y in
MkVar (Later prf)
weakenVar : (ns : List Name) -> IsVar name idx inner ->
(idx' ** IsVar name idx' (ns ++ inner))
weakenVar [] x = (_ ** x)
weakenVar : (ns : List Name) -> {idx : Nat} -> .(IsVar name idx inner) ->
Var (ns ++ inner)
weakenVar [] x = MkVar x
weakenVar (y :: xs) x
= let (_ ** x') = weakenVar xs x in
(_ ** Later x')
= let MkVar x' = weakenVar xs x in
MkVar (Later x')
export
insertVarNames : {outer, ns : _} ->
(idx : _) ->
IsVar name idx (outer ++ inner) ->
(idx' ** IsVar name idx' (outer ++ (ns ++ inner)))
(idx : Nat) ->
.(IsVar name idx (outer ++ inner)) ->
Var (outer ++ (ns ++ inner))
insertVarNames {ns} {outer = []} idx prf = weakenVar ns prf
insertVarNames {outer = (y :: xs)} Z First = (_ ** First)
insertVarNames {outer = (y :: xs)} Z First = MkVar First
insertVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
= let (_ ** prf) = insertVarNames {ns} i x in
(_ ** Later prf)
= let MkVar prf = insertVarNames {ns} i x in
MkVar (Later prf)
export
thin : {outer, inner : _} ->
(n : Name) -> Term (outer ++ inner) -> Term (outer ++ n :: inner)
thin n (Local fc r idx prf)
= let (idx' ** var') = insertVar {n} idx prf in
Local fc r idx' var'
= let MkVar var' = insertVar {n} idx prf in
Local fc r _ var'
thin n (Ref fc nt name) = Ref fc nt name
thin n (Meta fc name idx args) = Meta fc name idx (map (thin n) args)
thin {outer} {inner} n (Bind fc x b scope)
@ -471,7 +475,7 @@ insertNames : {outer, inner : _} ->
(ns : List Name) -> Term (outer ++ inner) ->
Term (outer ++ (ns ++ inner))
insertNames ns (Local fc r idx prf)
= let (_ ** prf') = insertVarNames {ns} idx prf in
= let MkVar prf' = insertVarNames {ns} idx prf in
Local fc r _ prf'
insertNames ns (Ref fc nt name) = Ref fc nt name
insertNames ns (Meta fc name idx args)
@ -490,16 +494,6 @@ insertNames ns (PrimVal fc c) = PrimVal fc c
insertNames ns (Erased fc) = Erased fc
insertNames ns (TType fc) = TType fc
thinVar : (n : Name) -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
thinVar n (MkVar prf)
= let (_ ** prf') = insertVar {n} _ prf in
MkVar prf'
insertNamesVar : (ns : List Name) -> Var (outer ++ inner) -> Var (outer ++ (ns ++ inner))
insertNamesVar ns (MkVar prf)
= let (_ ** prf') = insertVarNames {ns} _ prf in
MkVar prf'
export
Weaken Term where
weaken tm = thin {outer = []} _ tm
@ -525,22 +519,26 @@ extendCompats : (args : List Name) ->
extendCompats [] prf = prf
extendCompats (x :: xs) prf = CompatExt (extendCompats xs prf)
renameLocalRef : CompatibleVars xs ys -> IsVar name idx xs -> (name' ** IsVar name' idx ys)
renameLocalRef CompatPre First = (_ ** First)
renameLocalRef (CompatExt x) First = (_ ** First)
renameLocalRef CompatPre (Later p) = (_ ** Later p)
renameLocalRef : CompatibleVars xs ys ->
{idx : Nat} ->
.(IsVar name idx xs) ->
Var ys
renameLocalRef CompatPre First = (MkVar First)
renameLocalRef (CompatExt x) First = (MkVar First)
renameLocalRef CompatPre (Later p) = (MkVar (Later p))
renameLocalRef (CompatExt y) (Later p)
= let (_ ** p') = renameLocalRef y p in (_ ** Later p')
= let (MkVar p') = renameLocalRef y p in MkVar (Later p')
renameVarList : CompatibleVars xs ys -> Var xs -> Var ys
renameVarList prf (MkVar p) = MkVar (snd (renameLocalRef prf p))
renameVarList prf (MkVar p) = renameLocalRef prf p
-- TODO: Surely identity at run time, can we replace with 'believe_me'?
export
renameVars : CompatibleVars xs ys -> Term xs -> Term ys
renameVars CompatPre tm = tm
renameVars prf (Local fc r idx vprf)
= Local fc r idx (snd (renameLocalRef prf vprf))
= let MkVar vprf' = renameLocalRef prf vprf in
Local fc r _ vprf'
renameVars prf (Ref fc x name) = Ref fc x name
renameVars prf (Meta fc n i args)
= Meta fc n i (map (renameVars prf) args)
@ -568,16 +566,17 @@ data SubVars : List Name -> List Name -> Type where
KeepCons : SubVars xs ys -> SubVars (x :: xs) (x :: ys)
export
subElem : IsVar name x xs -> SubVars ys xs -> Maybe (x' ** IsVar name x' ys)
subElem prf SubRefl = Just (_ ** prf)
subElem : {idx : Nat} -> .(IsVar name idx xs) ->
SubVars ys xs -> Maybe (Var ys)
subElem prf SubRefl = Just (MkVar prf)
subElem First (DropCons p) = Nothing
subElem (Later x) (DropCons p)
= do (_ ** prf') <- subElem x p
Just (_ ** prf')
subElem First (KeepCons p) = Just (_ ** First)
= do MkVar prf' <- subElem x p
Just (MkVar prf')
subElem First (KeepCons p) = Just (MkVar First)
subElem (Later x) (KeepCons p)
= do (_ ** prf') <- subElem x p
Just (_ ** Later prf')
= do MkVar prf' <- subElem x p
Just (MkVar (Later prf'))
export
subExtend : (ns : List Name) -> SubVars xs ys -> SubVars (ns ++ xs) (ns ++ ys)
@ -602,17 +601,14 @@ mutual
export
shrinkVar : Var vars -> SubVars newvars vars -> Maybe (Var newvars)
shrinkVar (MkVar x) prf
= case subElem x prf of
Nothing => Nothing
Just (_ ** x') => Just (MkVar x')
shrinkVar (MkVar x) prf = subElem x prf
export
shrinkTerm : Term vars -> SubVars newvars vars -> Maybe (Term newvars)
shrinkTerm (Local fc r idx loc) prf
= case subElem loc prf of
Nothing => Nothing
Just (_ ** loc') => Just (Local fc r _ loc')
Just (MkVar loc') => Just (Local fc r _ loc')
shrinkTerm (Ref fc x name) prf = Just (Ref fc x name)
shrinkTerm (Meta fc x y xs) prf
= do xs' <- traverse (\x => shrinkTerm x prf) xs
@ -639,13 +635,14 @@ data Bounds : List Name -> Type where
Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs)
addVars : {later, bound : _} ->
Bounds bound -> IsVar name idx (later ++ vars) ->
(idx' ** IsVar name idx' (later ++ (bound ++ vars)))
{idx : Nat} ->
Bounds bound -> .(IsVar name idx (later ++ vars)) ->
Var (later ++ (bound ++ vars))
addVars {later = []} {bound} bs p = weakenVar bound p
addVars {later = (x :: xs)} bs First = (_ ** First)
addVars {later = (x :: xs)} bs First = MkVar First
addVars {later = (x :: xs)} bs (Later p)
= let (_ ** p') = addVars {later = xs} bs p in
(_ ** Later p')
= let MkVar p' = addVars {later = xs} bs p in
MkVar (Later p')
resolveRef : (done : List Name) -> Bounds bound -> FC -> Name ->
Maybe (Term (later ++ (done ++ bound ++ vars)))
@ -653,23 +650,17 @@ resolveRef done None fc n = Nothing
resolveRef {later} {vars} done (Add {xs} new old bs) fc n
= if n == old
then rewrite appendAssociative later done (new :: xs ++ vars) in
let (_ ** p) = weakenVar {inner = new :: xs ++ vars}
(later ++ done) First in
let MkVar p = weakenVar {inner = new :: xs ++ vars}
(later ++ done) First in
Just (Local fc Nothing _ p)
else rewrite appendAssociative done [new] (xs ++ vars)
in resolveRef (done ++ [new]) bs fc n
mkLocalVar : {later, bound : _} ->
Bounds bound ->
Var (later ++ vars) -> Var (later ++ (bound ++ vars))
mkLocalVar bs (MkVar p)
= let (_ ** p') = addVars bs p in MkVar p'
mkLocals : {later, bound : _} ->
Bounds bound ->
Term (later ++ vars) -> Term (later ++ (bound ++ vars))
mkLocals bs (Local fc r idx p)
= let (_ ** p') = addVars bs p in Local fc r _ p'
= let MkVar p' = addVars bs p in Local fc r _ p'
mkLocals bs (Ref fc Bound name)
= maybe (Ref fc Bound name) id (resolveRef [] bs fc name)
mkLocals bs (Ref fc nt name)
@ -699,20 +690,20 @@ refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
refsToLocals bs y = mkLocals {later = []} bs y
export
isVar : (n : Name) -> (ns : List Name) -> Maybe (idx ** IsVar n idx ns)
isVar : (n : Name) -> (ns : List Name) -> Maybe (Var ns)
isVar n [] = Nothing
isVar n (m :: ms)
= case nameEq n m of
Nothing => do (_ ** p) <- isVar n ms
pure (_ ** Later p)
Just Refl => pure (_ ** First)
Nothing => do MkVar p <- isVar n ms
pure (MkVar (Later p))
Just Refl => pure (MkVar First)
-- Replace any Ref Bound in a type with appropriate local
export
resolveNames : (vars : List Name) -> Term vars -> Term vars
resolveNames vars (Ref fc Bound name)
= case isVar name vars of
Just (_ ** prf) => Local fc Nothing _ prf
Just (MkVar prf) => Local fc Nothing _ prf
_ => Ref fc Bound name
resolveNames vars (Meta fc n i xs)
= Meta fc n i (map (resolveNames vars) xs)
@ -741,16 +732,16 @@ namespace SubstEnv
(::) : Term vars ->
SubstEnv ds vars -> SubstEnv (d :: ds) vars
findDrop : {drop, idx : _} ->
FC -> Maybe RigCount -> IsVar name idx (drop ++ vars) ->
findDrop : {drop : _} -> {idx : Nat} ->
FC -> Maybe RigCount -> .(IsVar name idx (drop ++ vars)) ->
SubstEnv drop vars -> Term vars
findDrop {drop = []} fc r var env = Local fc r _ var
findDrop {drop = x :: xs} fc r First (tm :: env) = tm
findDrop {drop = x :: xs} fc r (Later p) (tm :: env)
= findDrop fc r p env
find : {outer, idx : _} ->
FC -> Maybe RigCount -> IsVar name idx (outer ++ (drop ++ vars)) ->
find : {outer : _} -> {idx : Nat} ->
FC -> Maybe RigCount -> .(IsVar name idx (outer ++ (drop ++ vars))) ->
SubstEnv drop vars ->
Term (outer ++ vars)
find {outer = []} fc r var env = findDrop fc r var env

198
src/Core/TTC.idr
View File

@ -13,11 +13,12 @@ import Utils.Binary
export
TTC FC where
toBuf b (MkFC file startPos endPos)
= do toBuf b file; toBuf b startPos; toBuf b endPos
= pure () -- do toBuf b file; toBuf b startPos; toBuf b endPos
fromBuf r b
= do f <- fromBuf r b;
s <- fromBuf r b; e <- fromBuf r b
pure (MkFC f s e)
= pure emptyFC
-- do f <- fromBuf r b;
-- s <- fromBuf r b; e <- fromBuf r b
-- pure (MkFC f s e)
export
TTC Name where
@ -77,25 +78,6 @@ TTC PiInfo where
2 => pure AutoImplicit
_ => corrupt "PiInfo"
export
TTC ty => TTC (Binder ty) where
toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; toBuf b ty
toBuf b (Let c val ty) = do tag 1; toBuf b c; toBuf b val; toBuf b ty
toBuf b (Pi c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty
toBuf b (PVar c ty) = do tag 3; toBuf b c; toBuf b ty
toBuf b (PLet c val ty) = do tag 4; toBuf b c; toBuf b val; toBuf b ty
toBuf b (PVTy c ty) = do tag 5; toBuf b c; toBuf b ty
fromBuf r b
= case !getTag of
0 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Lam c x y)
1 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Let c x y)
2 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Pi c x y)
3 => do c <- fromBuf r b; x <- fromBuf r b; pure (PVar c x)
4 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (PLet c x y)
5 => do c <- fromBuf r b; x <- fromBuf r b; pure (PVTy c x)
_ => corrupt "Binder"
export
TTC Visibility where
toBuf b Private = tag 0
@ -193,76 +175,108 @@ TTC (Var vars) where
i <- fromBuf r b
pure (MkVar {n} (mkPrf i))
export
TTC (Term vars) where
toBuf b (Local {name} fc c idx y)
= do tag 0;
toBuf b fc; toBuf b name
toBuf b c; toBuf b idx
toBuf b (Ref fc nt name)
= do tag 1;
toBuf b fc; toBuf b nt; toBuf b name
toBuf b (Meta fc n i xs)
= do tag 2;
toBuf b fc; toBuf b n; toBuf b i; toBuf b xs
toBuf b (Bind fc x bnd scope)
= do tag 3;
toBuf b fc; toBuf b x; toBuf b bnd; toBuf b scope
toBuf b (App fc fn p arg)
= do tag 4;
toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg
toBuf b (As fc as tm)
= do tag 5;
toBuf b fc; toBuf b as; toBuf b tm
toBuf b (TDelayed fc r tm)
= do tag 6;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TDelay fc r tm)
= do tag 7;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TForce fc tm)
= do tag 8;
toBuf b fc; toBuf b tm
toBuf b (PrimVal fc c)
= do tag 9;
toBuf b fc; toBuf b c
toBuf b (Erased fc)
= do tag 10;
toBuf b fc
toBuf b (TType fc)
= do tag 11;
toBuf b fc
mutual
export
TTC (Binder (Term vars)) where
toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; -- toBuf b ty
toBuf b (Let c val ty) = do tag 1; toBuf b c; toBuf b val -- ; toBuf b ty
toBuf b (Pi c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty
toBuf b (PVar c ty) = do tag 3; toBuf b c -- ; toBuf b ty
toBuf b (PLet c val ty) = do tag 4; toBuf b c; toBuf b val -- ; toBuf b ty
toBuf b (PVTy c ty) = do tag 5; toBuf b c -- ; toBuf b ty
fromBuf r b
= case !getTag of
0 => do fc <- fromBuf r b; name <- fromBuf r b
c <- fromBuf r b; idx <- fromBuf r b
pure (Local {name} fc c idx (mkPrf idx))
1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b
pure (Ref fc nt name)
2 => do fc <- fromBuf r b; n <- fromBuf r b; i <- fromBuf r b
xs <- fromBuf r b
pure (Meta fc n i xs)
3 => do fc <- fromBuf r b; x <- fromBuf r b
bnd <- fromBuf r b; scope <- fromBuf r b
pure (Bind fc x bnd scope)
4 => do fc <- fromBuf r b; fn <- fromBuf r b
p <- fromBuf r b; arg <- fromBuf r b
pure (App fc fn p arg)
5 => do fc <- fromBuf r b
as <- fromBuf r b; tm <- fromBuf r b
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)
8 => do fc <- fromBuf r b; tm <- fromBuf r b
pure (TForce fc tm)
9 => do fc <- fromBuf r b; c <- fromBuf r b
pure (PrimVal fc c)
10 => do fc <- fromBuf r b; pure (Erased fc)
11 => do fc <- fromBuf r b; pure (TType fc)
_ => corrupt "Term"
fromBuf r b
= case !getTag of
0 => do c <- fromBuf r b; x <- fromBuf r b; pure (Lam c x (Erased emptyFC))
1 => do c <- fromBuf r b; x <- fromBuf r b; pure (Let c x (Erased emptyFC))
2 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Pi c x y)
3 => do c <- fromBuf r b; pure (PVar c (Erased emptyFC))
4 => do c <- fromBuf r b; x <- fromBuf r b; pure (PLet c x (Erased emptyFC))
5 => do c <- fromBuf r b; pure (PVTy c (Erased emptyFC))
_ => corrupt "Binder"
export
TTC (Term vars) where
toBuf b (Local {name} fc c idx y)
= if idx < 244
then toBuf b (prim__truncBigInt_B8 (12 + cast idx))
else do tag 0;
toBuf b fc -- toBuf b name
toBuf b idx
toBuf b (Ref fc nt name)
= do tag 1;
toBuf b fc; toBuf b nt; toBuf b name
toBuf b (Meta fc n i xs)
= do tag 2;
toBuf b fc -- Name no longer needed -- toBuf b n;
toBuf b i; toBuf b xs
toBuf b (Bind fc x bnd scope)
= do tag 3;
toBuf b fc; toBuf b x;
toBuf b bnd; toBuf b scope
toBuf b (App fc fn p arg)
= do tag 4;
let (fn, args) = getFnArgs (App fc fn p arg)
toBuf b fc; toBuf b fn; -- toBuf b p;
toBuf b (map snd args)
toBuf b (As fc as tm)
= do tag 5;
toBuf b fc; toBuf b as; toBuf b tm
toBuf b (TDelayed fc r tm)
= do tag 6;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TDelay fc r tm)
= do tag 7;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TForce fc tm)
= do tag 8;
toBuf b fc; toBuf b tm
toBuf b (PrimVal fc c)
= do tag 9;
toBuf b fc; toBuf b c
toBuf b (Erased fc)
= do tag 10;
toBuf b fc
toBuf b (TType fc)
= do tag 11;
toBuf b fc
fromBuf r b
= case !getTag of
0 => do fc <- fromBuf r b; -- name <- fromBuf r b
idx <- fromBuf r b
pure (Local {name=UN "_"} fc Nothing idx (mkPrf idx))
1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b
pure (Ref fc nt name)
2 => do fc <- fromBuf r b; -- n <- fromBuf r b
i <- fromBuf r b
xs <- fromBuf r b
pure (Meta fc (UN "metavar") i xs)
3 => do fc <- fromBuf r b; x <- fromBuf r b
bnd <- fromBuf r b; scope <- fromBuf r b
pure (Bind fc x bnd scope)
4 => do fc <- fromBuf r b; fn <- fromBuf r b
-- p <- fromBuf r b;
args <- fromBuf r b
pure (apply fc (explApp Nothing) fn args)
5 => do fc <- fromBuf r b
as <- fromBuf r b; tm <- fromBuf r b
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)
8 => do fc <- fromBuf r b; tm <- fromBuf r b
pure (TForce fc tm)
9 => do fc <- fromBuf r b; c <- fromBuf r b
pure (PrimVal fc c)
10 => do fc <- fromBuf r b; pure (Erased fc)
11 => do fc <- fromBuf r b; pure (TType fc)
idxp => do -- fc <- fromBuf r b; -- name <- fromBuf r b
let idx = fromInteger (prim__sextB8_BigInt idxp - 12)
pure (Local {name=UN "_"}
emptyFC Nothing idx (mkPrf idx))
export
TTC Pat where

10
src/Core/Unify.idr
View File

@ -219,7 +219,7 @@ patternEnv env args
updateVars (MkVar p :: ps) svs
= case subElem p svs of
Nothing => updateVars ps svs
Just (_ ** p') => MkVar p' :: updateVars ps svs
Just p' => p' :: updateVars ps svs
-- Instantiate a metavariable by binding the variables in 'newvars'
-- and returning the term
@ -249,7 +249,7 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
(record { definition = PMDef [] (STerm rhs) (STerm rhs) [] } mdef)
removeHole mref
where
updateLoc : List (Var vs) -> IsVar name v vs' ->
updateLoc : {v : Nat} -> List (Var vs) -> .(IsVar name v vs') ->
Maybe (Var vs)
updateLoc [] el = Nothing
updateLoc (p :: ps) First = Just p
@ -293,7 +293,7 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
(rewrite appendAssociative vs [v] got in locs)
(rewrite appendAssociative vs [v] got in tm)
sc
pure (Bind bfc x (Lam c Explicit ty) sc')
pure (Bind bfc x (Lam c Explicit (Erased bfc)) sc')
mkDef got (vs ++ [v]) (Snoc rec) cvs locs tm ty = Nothing
@ -619,14 +619,14 @@ retry mode c
=> catch (do log 5 $ "Retrying " ++ show x ++ " and " ++ show y
cs <- unify mode loc env x y
case constraints cs of
[] => do setConstraint c Resolved
[] => do deleteConstraint c
pure success
_ => pure cs)
(\err => throw (WhenUnifying loc env x y err))
Just (MkSeqConstraint loc env xs ys)
=> do cs <- unifyArgs mode loc env xs ys
case constraints cs of
[] => do setConstraint c Resolved
[] => do deleteConstraint c
pure success
_ => pure cs

48
src/Core/UnifyState.idr
View File

@ -116,6 +116,16 @@ removeHole n
put UST (record { holes $= delete n,
currentHoles $= delete n } ust)
export
removeHoleName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Name -> Core ()
removeHoleName n
= do defs <- get Ctxt
let Just i = getNameID n (gamma defs)
| Nothing => pure ()
removeHole i
export
saveHoles : {auto u : Ref UST UState} ->
Core (IntMap (FC, Name))
@ -178,6 +188,20 @@ getCurrentHoles
= do ust <- get UST
pure (currentHoles ust)
export
isHole : {auto u : Ref UST UState} ->
Int -> Core Bool
isHole i
= do ust <- get UST
pure (maybe False (const True) (lookup i (holes ust)))
export
isCurrentHole : {auto u : Ref UST UState} ->
Int -> Core Bool
isCurrentHole i
= do ust <- get UST
pure (maybe False (const True) (lookup i (currentHoles ust)))
export
setConstraint : {auto u : Ref UST UState} ->
Int -> Constraint -> Core ()
@ -185,6 +209,13 @@ setConstraint cid c
= do ust <- get UST
put UST (record { constraints $= insert cid c } ust)
export
deleteConstraint : {auto u : Ref UST UState} ->
Int -> Core ()
deleteConstraint cid
= do ust <- get UST
put UST (record { constraints $= delete cid } ust)
export
addConstraint : {auto u : Ref UST UState} ->
{auto c : Ref Ctxt Defs} ->
@ -345,20 +376,21 @@ checkUserHoles : {auto u : Ref UST UState} ->
{auto c : Ref Ctxt Defs} ->
Bool -> Core ()
checkUserHoles now
= do hs_map <- getCurrentHoles
gs_map <- getGuesses
let hs = toList hs_map
= do gs_map <- getGuesses
let gs = toList gs_map
log 10 $ "Unsolved guesses " ++ show gs
traverse checkValidHole gs
let hs' = if not now || any isUserName (map (snd . snd) hs)
then [] else hs
when (not (isNil hs')) $
throw (UnsolvedHoles (map snd (nubBy nameEq hs)))
if now
then do hs_map <- getCurrentHoles
let hs = toList hs_map
let hs' = if any isUserName (map (snd . snd) hs)
then [] else hs
when (not (isNil hs')) $
throw (UnsolvedHoles (map snd (nubBy nameEq hs)))
else pure ()
-- Note the hole names, to ensure they are resolved
-- by the end of elaborating the current source file
-- traverse (\x => addDelayedHoleName (fst x) (snd x)) hs'
pure ()
where
nameEq : (a, b, Name) -> (a, b, Name) -> Bool
nameEq (_, _, x) (_, _, y) = x == y

1
src/TTImp/Elab.idr
View File

@ -38,6 +38,7 @@ elabTerm defining mode env tm ty
InLHS _ => InLHS
_ => InTerm) LastChance
checkNoGuards -- all unification problems must now be solved
-- checkUserHoles True -- TODO on everything but types!
pure (chktm, chkty)
export

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

@ -21,7 +21,7 @@ getNameType : {vars : _} ->
Core (Term vars, Glued vars)
getNameType rigc env fc x expected
= case defined x env of
Just (_ ** (rigb, lv)) =>
Just (MkIsDefined rigb lv) =>
do rigSafe rigb rigc
defs <- get Ctxt
let bty = binderType (getBinder lv env)
@ -146,6 +146,7 @@ mutual
[] <- convert fc elabinfo env (gnf defs env metaval)
(gnf defs env argv)
| cs => throw (CantConvert fc env metaval argv)
removeHoleName nm
pure (tm, gty)
else do
defs <- get Ctxt

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

@ -17,24 +17,22 @@ import Data.NameMap
%default covering
varEmbedSub : SubVars small vars -> IsVar n idx small ->
(idx' ** IsVar n idx' vars)
varEmbedSub SubRefl y = (_ ** y)
varEmbedSub : SubVars small vars ->
{idx : Nat} -> .(IsVar n idx small) ->
Var vars
varEmbedSub SubRefl y = MkVar y
varEmbedSub (DropCons prf) y
= let (_ ** y') = varEmbedSub prf y in
(_ ** Later y')
varEmbedSub (KeepCons prf) First = (_ ** First)
= let MkVar y' = varEmbedSub prf y in
MkVar (Later y')
varEmbedSub (KeepCons prf) First = MkVar First
varEmbedSub (KeepCons prf) (Later p)
= let (_ ** p') = varEmbedSub prf p in
(_ ** Later p')
embedVar : SubVars small vars -> Var small -> Var vars
embedVar sub (MkVar x) = let (_ ** x') = varEmbedSub sub x in MkVar x'
= let MkVar p' = varEmbedSub prf p in
MkVar (Later p')
mutual
embedSub : SubVars small vars -> Term small -> Term vars
embedSub sub (Local fc x idx y)
= let (_ ** y') = varEmbedSub sub y in Local fc x _ y'
= let MkVar y' = varEmbedSub sub y in Local fc x _ y'
embedSub sub (Ref fc x name) = Ref fc x name
embedSub sub (Meta fc x y xs)
= Meta fc x y (map (embedSub sub) xs)
@ -76,6 +74,7 @@ mkOuterHole loc rig n topenv Nothing
let env = outerEnv est
nm <- genName "impty"
ty <- metaVar loc Rig0 env nm (TType loc)
log 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm
put EST (addBindIfUnsolved nm rig topenv (embedSub sub ty) (TType loc) est)
tm <- metaVar loc rig env n ty
pure (embedSub sub tm, embedSub sub ty)
@ -85,7 +84,6 @@ mkOuterHole loc rig n topenv Nothing
-- Returns the hole term, its expected type (this is the type we'll use when
-- we see the name later) and the type the binder will need to be when we
-- instantiate it.
export
mkPatternHole : {auto e : Ref EST (EState vars)} ->
{auto c : Ref Ctxt Defs} ->
{auto e : Ref UST UState} ->
@ -139,7 +137,7 @@ bindUnsolved {vars} fc elabmode _
= do est <- get EST
defs <- get Ctxt
let bifs = bindIfUnsolved est
log 10 $ "Bindable unsolved implicits: " ++ show (map fst bifs)
log 5 $ "Bindable unsolved implicits: " ++ show (map fst bifs)
traverse (mkImplicit defs (outerEnv est) (subEnv est)) (bindIfUnsolved est)
pure ()
where
@ -175,24 +173,24 @@ bindUnsolved {vars} fc elabmode _
fc env tm bindtm
pure ()
swapIsVarH : IsVar name idx (x :: y :: xs) ->
(idx' ** IsVar name idx' (y :: x :: xs))
swapIsVarH First = (_ ** Later First)
swapIsVarH (Later First) = (_ ** First)
swapIsVarH (Later (Later x)) = (_ ** Later (Later x))
swapIsVarH : {idx : Nat} -> .(IsVar name idx (x :: y :: xs)) ->
Var (y :: x :: xs)
swapIsVarH First = MkVar (Later First)
swapIsVarH (Later First) = MkVar First
swapIsVarH (Later (Later x)) = MkVar (Later (Later x))
swapIsVar : (vs : List Name) ->
IsVar name idx (vs ++ x :: y :: xs) ->
(idx' ** IsVar name idx' (vs ++ y :: x :: xs))
{idx : Nat} -> .(IsVar name idx (vs ++ x :: y :: xs)) ->
Var (vs ++ y :: x :: xs)
swapIsVar [] prf = swapIsVarH prf
swapIsVar (x :: xs) First = (_ ** First)
swapIsVar (x :: xs) First = MkVar First
swapIsVar (x :: xs) (Later p)
= let (_ ** p') = swapIsVar xs p in (_ ** Later p')
= let MkVar p' = swapIsVar xs p in MkVar (Later p')
swapVars : {vs : List Name} ->
Term (vs ++ x :: y :: ys) -> Term (vs ++ y :: x :: ys)
swapVars (Local fc x idx p)
= let (_ ** p') = swapIsVar _ p in Local fc x _ p'
= let MkVar p' = swapIsVar _ p in Local fc x _ p'
swapVars (Ref fc x name) = Ref fc x name
swapVars (Meta fc n i xs) = Meta fc n i (map swapVars xs)
swapVars {vs} (Bind fc x b scope)
@ -297,6 +295,7 @@ implicitBind n
Just (Hole _) <- lookupDefExact n (gamma defs)
| _ => pure ()
updateDef n (const (Just ImpBind))
removeHoleName n
-- 'toBind' are the names which are to be implicitly bound (pattern bindings and
-- unbound implicits).
@ -334,24 +333,29 @@ getToBind {vars} fc elabmode impmode env excepts toptm
Core (List (Name, Term vars))
normImps defs ns [] = pure []
normImps defs ns ((PV n i, tm, ty) :: ts)
= if PV n i `elem` ns
then normImps defs ns ts
else do rest <- normImps defs (PV n i :: ns) ts
pure ((PV n i, !(normaliseHoles defs env ty)) :: rest)
= do logTermNF 10 ("Implicit pattern var " ++ show (PV n i)) env ty
if PV n i `elem` ns
then normImps defs ns ts
else do rest <- normImps defs (PV n i :: ns) ts
pure ((PV n i, !(normaliseHoles defs env ty)) :: rest)
normImps defs ns ((n, tm, ty) :: ts)
= do tmnf <- normaliseHoles defs env tm
logTerm 10 ("Normalising implicit " ++ show n) tmnf
case getFnArgs tmnf of
-- n reduces to another hole, n', so treat it as that as long
-- as it isn't already done
(Meta _ n' i margs, args) =>
if not (n' `elem` ns)
then do rest <- normImps defs (n' :: ns) ts
tynf <- normaliseHoles defs env ty
pure ((n', tynf) :: rest)
else normImps defs ns ts
_ => do rest <- normImps defs (n :: ns) ts
tynf <- normaliseHoles defs env ty
pure ((n, tynf) :: rest)
do hole <- isCurrentHole i
if hole && not (n' `elem` ns)
then do rest <- normImps defs (n' :: ns) ts
tynf <- normaliseHoles defs env ty
pure ((n', tynf) :: rest)
else normImps defs ns ts
_ => -- Unified to something concrete, so drop it
normImps defs ns ts
-- _ => do rest <- normImps defs (n :: ns) ts
-- tynf <- normaliseHoles defs env ty
-- pure ((n, tynf) :: rest)
-- Insert the hole/binding pair into the list before the first thing
-- which refers to it

1
src/TTImp/ProcessData.idr
View File

@ -83,6 +83,7 @@ processData env fc vis (MkImpLater dfc n_in ty_raw)
pure ()
processData 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 n InType env (IBindHere fc (PI Rig0) ty_raw)
(Just (gType dfc))

19
src/TTImp/ProcessDecls.idr
View File

@ -5,6 +5,9 @@ import Core.Core
import Core.Env
import Core.UnifyState
import Parser.Support
import TTImp.Parser
import TTImp.ProcessData
import TTImp.ProcessDef
import TTImp.ProcessType
@ -31,3 +34,19 @@ processDecls : {vars : _} ->
processDecls env decls
= do traverse (processDecl env) decls
pure True -- TODO: False on error
export
processTTImpFile : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
String -> Core Bool
processTTImpFile fname
= do Right tti <- coreLift $ parseFile fname
(do decls <- prog fname
eoi
pure decls)
| Left err => do coreLift (putStrLn (show err))
pure False
catch (do processDecls [] tti
pure True)
(\err => do coreLift (printLn err)
pure False)

1
src/TTImp/ProcessType.idr
View File

@ -19,6 +19,7 @@ processType : {vars : _} ->
List FnOpt -> ImpTy -> Core ()
processType env fc rig vis opts (MkImpTy tfc n_in ty_raw)
= do n <- inCurrentNS n_in
log 1 $ "Processing " ++ show n
log 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw
(ty, _) <- elabTerm n InType env
(IBindHere fc (PI Rig0) ty_raw)

19
src/Utils/Binary.idr
View File

@ -144,11 +144,14 @@ interface TTC a where -- TTC = TT intermediate code/interface file
-- Throws if the data can't be parsed as an 'a'
fromBuf : NameRefs -> Ref Bin Binary -> Core a
blockSize : Int
blockSize = 655360
-- Create a new list of chunks, initialised with one 64k chunk
export
initBinary : Core (Ref Bin Binary)
initBinary
= do Just buf <- coreLift $ newBuffer 65536
= do Just buf <- coreLift $ newBuffer blockSize
| Nothing => throw (InternalError "Buffer creation failed")
newRef Bin (MkBin [] (newChunk buf) [])
@ -173,7 +176,7 @@ TTC Bits8 where
do coreLift $ setByte (buf chunk) (loc chunk) val
put Bin (MkBin done (appended 1 chunk) rest)
else
do Just newbuf <- coreLift $ newBuffer 65536
do Just newbuf <- coreLift $ newBuffer blockSize
| Nothing => throw (InternalError "Buffer expansion failed")
coreLift $ setByte newbuf 0 val
put Bin (MkBin (chunk :: done)
@ -215,7 +218,7 @@ TTC Int where
do coreLift $ setInt (buf chunk) (loc chunk) val
put Bin (MkBin done (appended 4 chunk) rest)
else
do Just newbuf <- coreLift $ newBuffer 65536
do Just newbuf <- coreLift $ newBuffer blockSize
| Nothing => throw (InternalError "Buffer expansion failed")
coreLift $ setInt newbuf 0 val
put Bin (MkBin (chunk :: done)
@ -247,7 +250,7 @@ TTC String where
do coreLift $ setString (buf chunk) (loc chunk) val
put Bin (MkBin done (appended req chunk) rest)
else
do Just newbuf <- coreLift $ newBuffer 65536
do Just newbuf <- coreLift $ newBuffer blockSize
| Nothing => throw (InternalError "Buffer expansion failed")
coreLift $ setString newbuf 0 val
put Bin (MkBin (chunk :: done)
@ -297,7 +300,7 @@ TTC Double where
do coreLift $ setDouble (buf chunk) (loc chunk) val
put Bin (MkBin done (appended 8 chunk) rest)
else
do Just newbuf <- coreLift $ newBuffer 65536
do Just newbuf <- coreLift $ newBuffer blockSize
| Nothing => throw (InternalError "Buffer expansion failed")
coreLift $ setDouble newbuf 0 val
put Bin (MkBin (chunk :: done)
@ -419,12 +422,12 @@ toLimbs x
= if x == 0
then []
else if x == -1 then [-1]
else fromInteger (prim__andBigInt x 0xff) ::
toLimbs (prim__ashrBigInt x 8)
else fromInteger (prim__andBigInt x 0xffffffff) ::
toLimbs (prim__ashrBigInt x 32)
fromLimbs : List Int -> Integer
fromLimbs [] = 0
fromLimbs (x :: xs) = cast x + prim__shlBigInt (fromLimbs xs) 8
fromLimbs (x :: xs) = cast x + prim__shlBigInt (fromLimbs xs) 32
export
TTC Integer where

9
src/Yaffle/Main.idr
View File

@ -29,14 +29,7 @@ coreMain fname
readFromTTC {extra = ()} emptyFC True fname [] []
coreLift $ putStrLn "Read TTC"
_ => do coreLift $ putStrLn "Processing as TTImp"
Right tti <- coreLift $ parseFile fname
(do decls <- prog fname
eoi
pure decls)
| Left err => do coreLift $ printLn err
coreLift $ exitWith (ExitFailure 1)
coreLift $ putStrLn "Parsed okay"
ok <- processDecls [] tti
ok <- processTTImpFile fname
when ok $
do makeBuildDirectory (pathToNS (working_dir d) fname)
writeToTTC () !(getTTCFileName fname ".ttc")

2
yaffle.ipkg
View File

@ -55,7 +55,7 @@ modules =
sourcedir = src
executable = yaffle
-- opts = "--partial-eval --cg-opt -O2"
-- opts = "--cg-opt -O2 --partial-eval yaffle.dc"
opts = "--partial-eval"
main = Yaffle.Main