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

Merge remote-tracking branch 'upstream/master' into misc-fixes

Browse Source
This commit is contained in:
Alex Gryzlov 2019-11-25 19:18:09 +03:00
commit 1652a6be7d
162 changed files with 3274 additions and 2385 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2.ipkg
View File

@ -110,6 +110,7 @@ modules =
TTImp.ProcessParams,
TTImp.ProcessRecord,
TTImp.ProcessType,
TTImp.Reflect,
TTImp.TTImp,
TTImp.Unelab,
TTImp.Utils,

2
libs/base/Data/Nat.idr
View File

@ -245,7 +245,7 @@ cmp (S x) (S y) with (cmp x y)
cmp (S x) (S x) | CmpEQ = CmpEQ
cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
-- Proofs on +
-- Proofs on
export
plusZeroLeftNeutral : (right : Nat) -> 0 + right = right

140
libs/base/Language/Reflection.idr
View File

@ -75,3 +75,143 @@ data TT : List Name -> Type where
Erased : FC -> TT vars
TType : FC -> TT vars
public export
data Visibility = Private | Export | Public
-- Unchecked terms and declarations in the intermediate language
mutual
public export
data BindMode = PI Count | PATTERN | NONE
-- For as patterns matching linear arguments, select which side is
-- consumed
public export
data UseSide = UseLeft | UseRight
data TTImp : Type where
IVar : FC -> Name -> TTImp
IPi : FC -> Count -> PiInfo -> Maybe Name ->
(argTy : TTImp) -> (retTy : TTImp) -> TTImp
ILam : FC -> Count -> PiInfo -> Maybe Name ->
(argTy : TTImp) -> (lamTy : TTImp) -> TTImp
ILet : FC -> Count -> Name ->
(nTy : TTImp) -> (nVal : TTImp) ->
(scope : TTImp) -> TTImp
ICase : FC -> TTImp -> (ty : TTImp) ->
List Clause -> TTImp
ILocal : FC -> List Decl -> TTImp -> TTImp
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
IApp : FC -> TTImp -> TTImp -> TTImp
IImplicitApp : FC -> TTImp -> Maybe Name -> TTImp -> TTImp
IWithApp : FC -> TTImp -> TTImp -> TTImp
ISearch : FC -> (depth : Nat) -> TTImp
IAlternative : FC -> AltType -> List TTImp -> TTImp
IRewrite : FC -> TTImp -> TTImp -> TTImp
-- Any implicit bindings in the scope should be bound here, using
-- the given binder
IBindHere : FC -> BindMode -> TTImp -> TTImp
-- A name which should be implicitly bound
IBindVar : FC -> String -> TTImp
-- An 'as' pattern, valid on the LHS of a clause only
IAs : FC -> UseSide -> Name -> TTImp -> TTImp
-- A 'dot' pattern, i.e. one which must also have the given value
-- by unification
IMustUnify : FC -> (reason : String) -> TTImp -> TTImp
-- Laziness annotations
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
IDelay : FC -> TTImp -> TTImp -- delay constructor
IForce : FC -> TTImp -> TTImp
IPrimVal : FC -> (c : Constant) -> TTImp
IType : FC -> TTImp
IHole : FC -> String -> TTImp
-- An implicit value, solved by unification, but which will also be
-- bound (either as a pattern variable or a type variable) if unsolved
-- at the end of elaborator
Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
public export
data IFieldUpdate : Type where
ISetField : (path : List String) -> TTImp -> IFieldUpdate
ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate
public export
data AltType : Type where
FirstSuccess : AltType
Unique : AltType
UniqueDefault : TTImp -> AltType
public export
data FnOpt : Type where
Inline : FnOpt
-- Flag means the hint is a direct hint, not a function which might
-- find the result (e.g. chasing parent interface dictionaries)
Hint : Bool -> FnOpt
-- Flag means to use as a default if all else fails
GlobalHint : Bool -> FnOpt
ExternFn : FnOpt
-- Defined externally, list calling conventions
ForeignFn : List String -> FnOpt
-- assume safe to cancel arguments in unification
Invertible : FnOpt
Total : FnOpt
Covering : FnOpt
PartialOK : FnOpt
public export
data ITy : Type where
MkTy : FC -> (n : Name) -> (ty : TTImp) -> ITy
public export
data DataOpt : Type where
SearchBy : List Name -> DataOpt -- determining arguments
NoHints : DataOpt -- Don't generate search hints for constructors
public export
data Data : Type where
MkData : FC -> (n : Name) -> (tycon : TTImp) ->
(opts : List DataOpt) ->
(datacons : List ITy) -> Data
MkLater : FC -> (n : Name) -> (tycon : TTImp) -> Data
public export
data IField : Type where
MkIField : FC -> Count -> PiInfo -> Name -> TTImp ->
IField
public export
data Record : Type where
MkRecord : FC -> (n : Name) ->
(params : List (Name, TTImp)) ->
(conName : Maybe Name) ->
(fields : List IField) ->
Record
public export
data Clause : Type where
PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
WithClause : FC -> (lhs : TTImp) -> (wval : TTImp) ->
List Clause -> Clause
ImpossibleClause : FC -> (lhs : TTImp) -> Clause
public export
data Decl : Type where
IClaim : FC -> Count -> Visibility -> List FnOpt ->
ITy -> Decl
IData : FC -> Visibility -> Data -> Decl
IDef : FC -> Name -> List Clause -> Decl
IParameters : FC -> List (Name, TTImp) ->
List Decl -> Decl
IRecord : FC -> Visibility -> Record -> Decl
INamespace : FC ->
(nested : Bool) ->
-- ^ if True, parent namespaces in the same file can also
-- look inside and see private/export names in full
List String -> List Decl -> Decl
ITransform : FC -> TTImp -> TTImp -> Decl
ILog : Nat -> Decl

23
libs/prelude/PrimIO.idr
View File

@ -10,10 +10,23 @@ export
data IO : Type -> Type where
MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
public export
PrimIO : Type -> Type
PrimIO a = (1 x : %World) -> IORes a
export
prim_io_pure : a -> PrimIO a
prim_io_pure x = \w => MkIORes x w
export
io_pure : a -> IO a
io_pure x = MkIO (\w => MkIORes x w)
export
prim_io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b
prim_io_bind fn k w
= let MkIORes x' w' = fn w in k x' w'
export
io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
io_bind (MkIO fn)
@ -21,10 +34,6 @@ io_bind (MkIO fn)
MkIO res = k x' in
res w')
public export
PrimIO : Type -> Type
PrimIO a = (1 x : %World) -> IORes a
%extern prim__putStr : String -> (1 x : %World) -> IORes ()
%extern prim__getStr : (1 x : %World) -> IORes String
@ -56,7 +65,7 @@ primIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
primIO op = MkIO op
export %inline
toPrim : IO a -> PrimIO a
toPrim : (1 act : IO a) -> PrimIO a
toPrim (MkIO fn) = fn
export %inline
@ -83,6 +92,10 @@ export
fork : (1 prog : IO ()) -> IO ThreadID
fork (MkIO act) = schemeCall ThreadID "blodwen-thread" [act]
export
prim_fork : (1 prog : PrimIO ()) -> PrimIO ThreadID
prim_fork act w = prim__schemeCall ThreadID "blodwen-thread" [act] w
unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a
unsafeCreateWorld f = f %MkWorld

2
src/Compiler/CompileExpr.idr
View File

@ -175,7 +175,7 @@ mutual
toCExpTm tags n (TDelayed fc _ _) = pure $ CErased fc
toCExpTm tags n (TDelay fc _ _ arg)
= pure (CDelay fc !(toCExp tags n arg))
toCExpTm tags n (TForce fc arg)
toCExpTm tags n (TForce fc _ arg)
= pure (CForce fc !(toCExp tags n arg))
toCExpTm tags n (PrimVal fc c)
= let t = constTag c in

BIN
src/Core/.Context.idr.swp Normal file
View File

Binary file not shown.

BIN
src/Core/.Normalise.idr.swp Normal file
View File

Binary file not shown.

2
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 9
ttcVersion = 10
export
checkTTCVersion : Int -> Int -> Core ()

53
src/Core/Context.idr
View File

@ -429,6 +429,23 @@ newDef fc n rig vars ty vis def
= MkGlobalDef fc n ty [] rig vars vis unchecked [] empty False False False def
Nothing []
-- Rewrite rules, applied after type checking, for runtime code only
-- LHS and RHS must have the same type, but we don't (currently) require that
-- the result still type checks (which might happen e.g. if transforming to a
-- faster implementation with different behaviour)
-- (Q: Do we need the 'Env' here? Usually we end up needing an 'Env' with a
-- 'NF but we're working with terms rather than values...)
public export
data Transform : Type where
MkTransform : Env Term vars -> Term vars -> Term vars -> Transform
export
getFnName : Transform -> Maybe Name
getFnName (MkTransform _ app _)
= case getFn app of
Ref _ _ fn => Just fn
_ => Nothing
public export
interface HasNames a where
full : Context -> a -> Core a
@ -469,8 +486,8 @@ HasNames (Term vars) where
= pure (TDelayed fc x !(full gam y))
full gam (TDelay fc x t y)
= pure (TDelay fc x !(full gam t) !(full gam y))
full gam (TForce fc y)
= pure (TForce fc !(full gam y))
full gam (TForce fc r y)
= pure (TForce fc r !(full gam y))
full gam tm = pure tm
resolved gam (Ref fc x n)
@ -492,8 +509,8 @@ HasNames (Term vars) where
= pure (TDelayed fc x !(resolved gam y))
resolved gam (TDelay fc x t y)
= pure (TDelay fc x !(resolved gam t) !(resolved gam y))
resolved gam (TForce fc y)
= pure (TForce fc !(resolved gam y))
resolved gam (TForce fc r y)
= pure (TForce fc r !(resolved gam y))
resolved gam tm = pure tm
mutual
@ -673,6 +690,15 @@ HasNames GlobalDef where
sizeChange = !(traverse (resolved gam) (sizeChange def))
} def
export
HasNames Transform where
full gam (MkTransform env lhs rhs)
= pure $ MkTransform !(full gam env) !(full gam lhs) !(full gam rhs)
resolved gam (MkTransform env lhs rhs)
= pure $ MkTransform !(resolved gam env)
!(resolved gam lhs) !(resolved gam rhs)
public export
record Defs where
constructor MkDefs
@ -701,6 +727,10 @@ record Defs where
-- We don't look up anything in here, it's merely for saving out to TTC.
-- We save the hints in the 'GlobalDef' itself for faster lookup.
saveAutoHints : List (Name, Bool)
transforms : NameMap Transform
-- ^ A mapping from names to transformation rules which update applications
-- of that name
saveTransforms : List (Name, Transform)
namedirectives : List (Name, List String)
ifaceHash : Int
importHashes : List (List String, Int)
@ -737,8 +767,8 @@ initDefs : Core Defs
initDefs
= do gam <- initCtxt
pure (MkDefs gam [] ["Main"] [] defaults empty 100
empty empty empty [] [] [] 5381 [] [] [] [] [] empty
empty)
empty empty empty [] [] empty []
[] 5381 [] [] [] [] [] empty empty)
-- Reset the context, except for the options
export
@ -1298,6 +1328,17 @@ setOpenHints hs
= do d <- get Ctxt
put Ctxt (record { openHints = hs } d)
export
addTransform : {auto c : Ref Ctxt Defs} ->
FC -> Transform -> Core ()
addTransform fc t
= do defs <- get Ctxt
let Just fn = getFnName t
| Nothing =>
throw (GenericMsg fc "LHS of a transformation must be a function application")
put Ctxt (record { transforms $= insert fn t,
saveTransforms $= ((fn, t) ::) } defs)
export
clearSavedHints : {auto c : Ref Ctxt Defs} -> Core ()
clearSavedHints

2
src/Core/Env.idr
View File

@ -153,7 +153,7 @@ mutual
= findUsed env used tm
findUsed env used (TDelay fc r ty tm)
= findUsed env (findUsed env used ty) tm
findUsed env used (TForce fc tm)
findUsed env used (TForce fc r tm)
= findUsed env used tm
findUsed env used _ = used

4
src/Core/GetType.idr
View File

@ -52,10 +52,10 @@ mutual
tm' <- getNF gtm
defs <- get Ctxt
pure $ glueBack defs env (NDelayed fc r tm')
chk env (TForce fc tm)
chk env (TForce fc r tm)
= do tm' <- chk env tm
case !(getNF tm') of
NDelayed fc r fty =>
NDelayed fc _ fty =>
do defs <- get Ctxt
pure $ glueBack defs env fty
chk env (PrimVal fc x) = pure $ gnf env (chkConstant fc x)

2
src/Core/Hash.idr
View File

@ -114,7 +114,7 @@ mutual
= h `hashWithSalt` 6 `hashWithSalt` y
hashWithSalt h (TDelay fc x t y)
= h `hashWithSalt` 7 `hashWithSalt` t `hashWithSalt` y
hashWithSalt h (TForce fc x)
hashWithSalt h (TForce fc r x)
= h `hashWithSalt` 8 `hashWithSalt` x
hashWithSalt h (PrimVal fc c)
= h `hashWithSalt` 9 `hashWithSalt` (show c)

6
src/Core/LinearCheck.idr
View File

@ -142,7 +142,7 @@ mutual
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TDelay _ _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TForce _ t)
updateHoleUsage useInHole var (TForce _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var tm
= case getFnArgs tm of
@ -305,13 +305,13 @@ mutual
(val', gty, u) <- lcheck rig erase env val
ty <- getTerm gty
pure (TDelay fc r ty' val', gnf env (TDelayed fc r ty), u)
lcheck rig erase env (TForce fc val)
lcheck rig erase env (TForce fc r val)
= do (val', gty, u) <- lcheck rig erase env val
tynf <- getNF gty
case tynf of
NDelayed _ r narg
=> do defs <- get Ctxt
pure (TForce fc val', glueBack defs env narg, u)
pure (TForce fc r 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, [])

20
src/Core/Normalise.idr
View File

@ -110,12 +110,12 @@ parameters (defs : Defs, topopts : EvalOpts)
eval env locs (TDelay fc r ty tm) stk
= pure (NDelay fc r (MkClosure topopts locs env ty)
(MkClosure topopts locs env tm))
eval env locs (TForce fc tm) stk
eval env locs (TForce fc r tm) stk
= do tm' <- eval env locs tm []
case tm' of
NDelay fc r _ arg =>
eval env (arg :: locs) (Local {name = UN "fvar"} fc Nothing _ First) stk
_ => pure (NForce fc tm' stk)
_ => pure (NForce fc r tm' stk)
eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c
eval env locs (Erased fc) stk = pure $ NErased fc
eval env locs (TType fc) stk = pure $ NType fc
@ -555,14 +555,14 @@ mutual
toHolesOnly (MkClosure _ locs env tm)
= MkClosure withHoles locs env tm
toHolesOnly c = c
quoteGenNF q defs bound env (NForce fc arg args)
quoteGenNF q defs bound env (NForce fc r arg args)
= do args' <- quoteArgs q defs bound env args
case arg of
NDelay fc _ _ arg =>
do argNF <- evalClosure defs arg
pure $ apply fc !(quoteGenNF q defs bound env argNF) args'
t => do arg' <- quoteGenNF q defs bound env arg
pure $ apply fc (TForce fc arg') args'
pure $ apply fc (TForce fc r arg') args'
quoteGenNF q defs bound env (NPrimVal fc c) = pure $ PrimVal fc c
quoteGenNF q defs bound env (NErased fc) = pure $ Erased fc
quoteGenNF q defs bound env (NType fc) = pure $ TType fc
@ -727,9 +727,11 @@ mutual
= if compatible r r'
then convGen q defs env arg arg'
else pure False
convGen q defs env (NForce _ arg args) (NForce _ arg' args')
= if !(convGen q defs env arg arg')
then allConv q defs env args args'
convGen q defs env (NForce _ r arg args) (NForce _ r' arg' args')
= if compatible r r'
then if !(convGen q defs env arg arg')
then allConv q defs env args args'
else pure False
else pure False
convGen q defs env (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
@ -887,10 +889,10 @@ replace' {vars} tmpi defs env lhs parg tm
= do ty' <- replace' tmpi defs env lhs parg !(evalClosure defs ty)
tm' <- replace' tmpi defs env lhs parg !(evalClosure defs tm)
pure (TDelay fc r ty' tm')
repSub (NForce fc tm args)
repSub (NForce fc r tm args)
= do args' <- traverse repArg args
tm' <- repSub tm
pure $ apply fc (TForce fc tm') args'
pure $ apply fc (TForce fc r tm') args'
repSub tm = do empty <- clearDefs defs
quote empty env tm

24
src/Core/Reflect.idr
View File

@ -3,8 +3,8 @@ module Core.Reflect
import Core.Context
import Core.Env
import Core.Normalise
import Core.Value
import Core.TT
import Core.Value
%default covering
@ -155,6 +155,23 @@ Reflect a => Reflect (List a) where
xs' <- reflect fc defs env xs
appCon fc defs (prelude "::") [Erased fc, x', xs']
export
Reify a => Reify (Maybe a) where
reify defs (NDCon _ (NS _ (UN "Nothing")) _ _ _)
= pure Nothing
reify defs (NDCon _ (NS _ (UN "Just")) _ _ [_, x])
= do x' <- reify defs !(evalClosure defs x)
pure (Just x')
reify defs val = cantReify val "Maybe"
export
Reflect a => Reflect (Maybe a) where
reflect fc defs env Nothing = appCon fc defs (prelude "Nothing") [Erased fc]
reflect fc defs env (Just x)
= do x' <- reflect fc defs env x
appCon fc defs (prelude "Just") [Erased fc, x']
export
(Reify a, Reify b) => Reify (a, b) where
reify defs (NDCon _ (NS _ (UN "MkPair")) _ _ [_, _, x, y])
@ -443,11 +460,12 @@ Reflect (Term vs) where
tm' <- reflect fc defs env tm
appCon fc defs (reflection "TDelay")
[Erased fc, dfc', r', ty', tm']
reflect fc defs env (TForce dfc tm)
reflect fc defs env (TForce dfc r tm)
= do dfc' <- reflect fc defs env dfc
r' <- reflect fc defs env r
tm' <- reflect fc defs env tm
appCon fc defs (reflection "TForce")
[Erased fc, dfc', tm']
[Erased fc, r', dfc', tm']
reflect fc defs env (PrimVal pfc c)
= do pfc' <- reflect fc defs env pfc
c' <- reflect fc defs env c

36
src/Core/TT.idr
View File

@ -394,7 +394,7 @@ data Term : List Name -> Type where
-- Typed laziness annotations
TDelayed : FC -> LazyReason -> Term vars -> Term vars
TDelay : FC -> LazyReason -> (ty : Term vars) -> (arg : Term vars) -> Term vars
TForce : FC -> Term vars -> Term vars
TForce : FC -> LazyReason -> Term vars -> Term vars
PrimVal : FC -> (c : Constant) -> Term vars
Erased : FC -> Term vars
TType : FC -> Term vars
@ -409,7 +409,7 @@ getLoc (App fc _ _) = fc
getLoc (As fc _ _) = fc
getLoc (TDelayed fc _ _) = fc
getLoc (TDelay fc _ _ _) = fc
getLoc (TForce fc _) = fc
getLoc (TForce fc _ _) = fc
getLoc (PrimVal fc _) = fc
getLoc (Erased fc) = fc
getLoc (TType fc) = fc
@ -449,7 +449,7 @@ Eq (Term vars) where
(==) (As _ a p) (As _ a' p') = a == a' && p == p'
(==) (TDelayed _ _ t) (TDelayed _ _ t') = t == t'
(==) (TDelay _ _ t x) (TDelay _ _ t' x') = t == t' && x == x'
(==) (TForce _ t) (TForce _ t') = t == t'
(==) (TForce _ _ t) (TForce _ _ t') = t == t'
(==) (PrimVal _ c) (PrimVal _ c') = c == c'
(==) (Erased _) (Erased _) = True
(==) (TType _) (TType _) = True
@ -625,7 +625,7 @@ thin n (App fc fn arg) = App fc (thin n fn) (thin n arg)
thin n (As fc nm tm) = As fc (thin n nm) (thin n tm)
thin n (TDelayed fc r ty) = TDelayed fc r (thin n ty)
thin n (TDelay fc r ty tm) = TDelay fc r (thin n ty) (thin n tm)
thin n (TForce fc tm) = TForce fc (thin n tm)
thin n (TForce fc r tm) = TForce fc r (thin n tm)
thin n (PrimVal fc c) = PrimVal fc c
thin n (Erased fc) = Erased fc
thin n (TType fc) = TType fc
@ -650,7 +650,7 @@ insertNames ns (As fc as tm)
insertNames ns (TDelayed fc r ty) = TDelayed fc r (insertNames ns ty)
insertNames ns (TDelay fc r ty tm)
= TDelay fc r (insertNames ns ty) (insertNames ns tm)
insertNames ns (TForce fc tm) = TForce fc (insertNames ns tm)
insertNames ns (TForce fc r tm) = TForce fc r (insertNames ns tm)
insertNames ns (PrimVal fc c) = PrimVal fc c
insertNames ns (Erased fc) = Erased fc
insertNames ns (TType fc) = TType fc
@ -765,7 +765,7 @@ renameVars prf (As fc as tm)
renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
renameVars prf (TDelay fc r ty tm)
= TDelay fc r (renameVars prf ty) (renameVars prf tm)
renameVars prf (TForce fc x) = TForce fc (renameVars prf x)
renameVars prf (TForce fc r x) = TForce fc r (renameVars prf x)
renameVars prf (PrimVal fc c) = PrimVal fc c
renameVars prf (Erased fc) = Erased fc
renameVars prf (TType fc) = TType fc
@ -845,8 +845,8 @@ mutual
= Just (TDelayed fc x !(shrinkTerm y prf))
shrinkTerm (TDelay fc x t y) prf
= Just (TDelay fc x !(shrinkTerm t prf) !(shrinkTerm y prf))
shrinkTerm (TForce fc x) prf
= Just (TForce fc !(shrinkTerm x prf))
shrinkTerm (TForce fc r x) prf
= Just (TForce fc r !(shrinkTerm x prf))
shrinkTerm (PrimVal fc c) prf = Just (PrimVal fc c)
shrinkTerm (Erased fc) prf = Just (Erased fc)
shrinkTerm (TType fc) prf = Just (TType fc)
@ -902,8 +902,8 @@ mkLocals bs (TDelayed fc x y)
= TDelayed fc x (mkLocals bs y)
mkLocals bs (TDelay fc x t y)
= TDelay fc x (mkLocals bs t) (mkLocals bs y)
mkLocals bs (TForce fc x)
= TForce fc (mkLocals bs x)
mkLocals bs (TForce fc r x)
= TForce fc r (mkLocals bs x)
mkLocals bs (PrimVal fc c) = PrimVal fc c
mkLocals bs (Erased fc) = Erased fc
mkLocals bs (TType fc) = TType fc
@ -946,8 +946,8 @@ resolveNames vars (TDelayed fc x y)
= TDelayed fc x (resolveNames vars y)
resolveNames vars (TDelay fc x t y)
= TDelay fc x (resolveNames vars t) (resolveNames vars y)
resolveNames vars (TForce fc x)
= TForce fc (resolveNames vars x)
resolveNames vars (TForce fc r x)
= TForce fc r (resolveNames vars x)
resolveNames vars tm = tm
@ -996,7 +996,7 @@ namespace SubstEnv
substEnv env (TDelayed fc x y) = TDelayed fc x (substEnv env y)
substEnv env (TDelay fc x t y)
= TDelay fc x (substEnv env t) (substEnv env y)
substEnv env (TForce fc x) = TForce fc (substEnv env x)
substEnv env (TForce fc r x) = TForce fc r (substEnv env x)
substEnv env (PrimVal fc c) = PrimVal fc c
substEnv env (Erased fc) = Erased fc
substEnv env (TType fc) = TType fc
@ -1030,8 +1030,8 @@ substName x new (TDelayed fc y z)
= TDelayed fc y (substName x new z)
substName x new (TDelay fc y t z)
= TDelay fc y (substName x new t) (substName x new z)
substName x new (TForce fc y)
= TForce fc (substName x new y)
substName x new (TForce fc r y)
= TForce fc r (substName x new y)
substName x new tm = tm
export
@ -1053,7 +1053,7 @@ addMetas ns (As fc as tm) = addMetas ns tm
addMetas ns (TDelayed fc x y) = addMetas ns y
addMetas ns (TDelay fc x t y)
= addMetas (addMetas ns t) y
addMetas ns (TForce fc x) = addMetas ns x
addMetas ns (TForce fc r x) = addMetas ns x
addMetas ns (PrimVal fc c) = ns
addMetas ns (Erased fc) = ns
addMetas ns (TType fc) = ns
@ -1088,7 +1088,7 @@ addRefs ua at ns (As fc as tm) = addRefs ua at ns tm
addRefs ua at ns (TDelayed fc x y) = addRefs ua at ns y
addRefs ua at ns (TDelay fc x t y)
= addRefs ua at (addRefs ua at ns t) y
addRefs ua at ns (TForce fc x) = addRefs ua at ns x
addRefs ua at ns (TForce fc r x) = addRefs ua at ns x
addRefs ua at ns (PrimVal fc c) = ns
addRefs ua at ns (Erased fc) = ns
addRefs ua at ns (TType fc) = ns
@ -1143,7 +1143,7 @@ export Show (Term vars) where
showApp (As _ n tm) [] = show n ++ "@" ++ show tm
showApp (TDelayed _ _ tm) [] = "%Delayed " ++ show tm
showApp (TDelay _ _ _ tm) [] = "%Delay " ++ show tm
showApp (TForce _ tm) [] = "%Force " ++ show tm
showApp (TForce _ _ tm) [] = "%Force " ++ show tm
showApp (PrimVal _ c) [] = show c
showApp (Erased _) [] = "[__]"
showApp (TType _) [] = "Type"

22
src/Core/TTC.idr
View File

@ -232,9 +232,9 @@ mutual
toBuf b (TDelay fc r ty tm)
= do tag 7;
toBuf b r; toBuf b ty; toBuf b tm
toBuf b (TForce fc tm)
toBuf b (TForce fc r tm)
= do tag 8;
toBuf b tm
toBuf b r; toBuf b tm
toBuf b (PrimVal fc c)
= do tag 9;
toBuf b c
@ -267,8 +267,8 @@ mutual
7 => do lr <- fromBuf b;
ty <- fromBuf b; tm <- fromBuf b
pure (TDelay emptyFC lr ty tm)
8 => do tm <- fromBuf b
pure (TForce emptyFC tm)
8 => do lr <- fromBuf b; tm <- fromBuf b
pure (TForce emptyFC lr tm)
9 => do c <- fromBuf b
pure (PrimVal emptyFC c)
10 => pure (Erased emptyFC)
@ -881,6 +881,20 @@ TTC GlobalDef where
RigW [] Public unchecked [] refs
False False True def cdef [])
TTC Transform where
toBuf b (MkTransform {vars} env lhs rhs)
= do toBuf b vars
toBuf b env
toBuf b lhs
toBuf b rhs
fromBuf b
= do vars <- fromBuf b
env <- fromBuf b
lhs <- fromBuf b
rhs <- fromBuf b
pure (MkTransform {vars} env lhs rhs)
-- decode : Context -> Int -> ContextEntry -> Core GlobalDef
Core.Context.decode gam idx (Coded bin)
= do b <- newRef Bin bin

12
src/Core/Termination.idr
View File

@ -49,7 +49,7 @@ scEq (As _ a p) p' = scEq p p'
scEq p (As _ a p') = scEq p p'
scEq (TDelayed _ _ t) (TDelayed _ _ t') = scEq t t'
scEq (TDelay _ _ t x) (TDelay _ _ t' x') = scEq t t' && scEq x x'
scEq (TForce _ t) (TForce _ t') = scEq t t'
scEq (TForce _ _ t) (TForce _ _ t') = scEq t t'
scEq (PrimVal _ c) (PrimVal _ c') = c == c'
scEq (Erased _) (Erased _) = True
scEq (TType _) (TType _) = True
@ -218,7 +218,7 @@ mutual
urhs (TDelayed fc r ty) = TDelayed fc r (updateRHS ms ty)
urhs (TDelay fc r ty tm)
= TDelay fc r (updateRHS ms ty) (updateRHS ms tm)
urhs (TForce fc tm) = TForce fc (updateRHS ms tm)
urhs (TForce fc r tm) = TForce fc r (updateRHS ms tm)
urhs (Bind fc x b sc)
= Bind fc x (map (updateRHS ms) b)
(updateRHS (map (\vt => (weaken (fst vt), weaken (snd vt))) ms) sc)
@ -278,8 +278,8 @@ mutual
rhs <- normaliseOpts tcOnly defs env tm
findSC defs env g pats rhs
-- Remove all laziness annotations which are nothing to do with coinduction,
-- meaning that all only Force/Delay left is to guard coinductive calls.
-- Remove all force and delay annotations which are nothing to do with
-- coinduction meaning that all Delays left guard coinductive calls.
delazy : Defs -> Term vars -> Term vars
delazy defs (TDelayed fc r tm)
= let tm' = delazy defs tm in
@ -292,6 +292,10 @@ delazy defs (TDelay fc r ty tm)
case r of
LInf => TDelay fc r ty' tm'
_ => tm'
delazy defs (TForce fc r t)
= case r of
LInf => TForce fc r (delazy defs t)
_ => delazy defs t
delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args)
delazy defs (Bind fc x b sc)
= Bind fc x (map (delazy defs) b) (delazy defs sc)

10
src/Core/Transform.idr Normal file
View File

@ -0,0 +1,10 @@
module Core.Transform
import Core.Context
import Core.Env
import Core.TT
export
applyTransforms : {auto c : Ref Ctxt Defs} ->
Term vars -> Core (Term vars)
applyTransforms t = pure t -- TODO!

18
src/Core/Unify.idr
View File

@ -32,12 +32,12 @@ Eq UnifyMode where
-- explicit force or delay to the first argument to unification. This says
-- which to add, if any. Can only added at the very top level.
public export
data AddLazy = NoLazy | AddForce | AddDelay LazyReason
data AddLazy = NoLazy | AddForce LazyReason | AddDelay LazyReason
export
Show AddLazy where
show NoLazy = "NoLazy"
show AddForce = "AddForce"
show (AddForce _) = "AddForce"
show (AddDelay _) = "AddDelay"
public export
@ -895,7 +895,7 @@ mutual
= unify mode loc env x y
unifyNoEta mode loc env (NDelay xfc _ xty x) (NDelay yfc _ yty y)
= unifyArgs mode loc env [xty, x] [yty, y]
unifyNoEta mode loc env (NForce xfc x axs) (NForce yfc y ays)
unifyNoEta mode loc env (NForce xfc _ x axs) (NForce yfc _ y ays)
= do cs <- unify mode loc env x y
cs' <- unifyArgs mode loc env axs ays
pure (union cs cs')
@ -984,7 +984,7 @@ mutual
= unify mode loc env tmx tmy
unifyWithLazyD _ _ mode loc env (NDelayed _ r tmx) tmy
= do vs <- unify mode loc env tmx tmy
pure (record { addLazy = AddForce } vs)
pure (record { addLazy = AddForce r } vs)
unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy)
= do vs <- unify mode loc env tmx tmy
pure (record { addLazy = AddDelay r } vs)
@ -1072,10 +1072,10 @@ delayMeta r (S k) ty (Bind fc n b sc)
= Bind fc n b (delayMeta r k (weaken ty) sc)
delayMeta r envb ty tm = TDelay (getLoc tm) r ty tm
forceMeta : Nat -> Term vars -> Term vars
forceMeta (S k) (Bind fc n b sc)
= Bind fc n b (forceMeta k sc)
forceMeta envb tm = TForce (getLoc tm) tm
forceMeta : LazyReason -> Nat -> Term vars -> Term vars
forceMeta r (S k) (Bind fc n b sc)
= Bind fc n b (forceMeta r k sc)
forceMeta r envb tm = TForce (getLoc tm) r tm
-- Retry the given constraint, return True if progress was made
retryGuess : {auto c : Ref Ctxt Defs} ->
@ -1117,7 +1117,7 @@ retryGuess mode smode (hid, (loc, hname))
case constraints cs of
[] => do tm' <- case addLazy cs of
NoLazy => pure tm
AddForce => pure $ forceMeta envb tm
AddForce r => pure $ forceMeta r envb tm
AddDelay r =>
do ty <- getType [] tm
pure $ delayMeta r envb !(getTerm ty) tm

4
src/Core/Value.idr
View File

@ -78,7 +78,7 @@ mutual
NAs : FC -> NF vars -> NF vars -> NF vars
NDelayed : FC -> LazyReason -> NF vars -> NF vars
NDelay : FC -> LazyReason -> Closure vars -> Closure vars -> NF vars
NForce : FC -> NF vars -> List (Closure vars) -> NF vars
NForce : FC -> LazyReason -> NF vars -> List (Closure vars) -> NF vars
NPrimVal : FC -> Constant -> NF vars
NErased : FC -> NF vars
NType : FC -> NF vars
@ -92,7 +92,7 @@ getLoc (NTCon fc _ _ _ _) = fc
getLoc (NAs fc _ _) = fc
getLoc (NDelayed fc _ _) = fc
getLoc (NDelay fc _ _ _) = fc
getLoc (NForce fc _ _) = fc
getLoc (NForce fc _ _ _) = fc
getLoc (NPrimVal fc _) = fc
getLoc (NErased fc) = fc
getLoc (NType fc) = fc

BIN
src/Idris/.Desugar.idr.swp Normal file
View File

Binary file not shown.

4
src/Idris/Desugar.idr
View File

@ -624,6 +624,10 @@ mutual
desugarDecl ps (PNamespace fc ns decls)
= do ds <- traverse (desugarDecl ps) decls
pure [INamespace fc False ns (concat ds)]
desugarDecl ps (PTransform fc lhs rhs)
= do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
rhs' <- desugar AnyExpr (bound ++ ps) rhs
pure [ITransform fc blhs rhs']
desugarDecl ps (PDirective fc d)
= case d of
Hide n => pure [IPragma (\c, nest, env => hide fc n)]

4
src/Idris/REPL.idr
View File

@ -420,7 +420,9 @@ process (Eval itm)
defs <- get Ctxt
opts <- get ROpts
let norm = nfun (evalMode opts)
itm <- resugar [] !(norm defs [] tm)
ntm <- norm defs [] tm
itm <- resugar [] ntm
logTermNF 5 "Normalised" [] ntm
if showTypes opts
then do ty <- getTerm gty
ity <- resugar [] !(norm defs [] ty)

3
src/Idris/Resugar.idr
View File

@ -337,6 +337,9 @@ mutual
toPDecl (INamespace fc _ ns ds)
= do ds' <- traverse toPDecl ds
pure (Just (PNamespace fc ns (mapMaybe id ds')))
toPDecl (ITransform fc lhs rhs)
= pure (Just (PTransform fc !(toPTerm startPrec lhs)
!(toPTerm startPrec rhs)))
toPDecl (IPragma _) = pure Nothing
toPDecl (ILog _) = pure Nothing

1
src/Idris/Syntax.idr
View File

@ -217,6 +217,7 @@ mutual
PMutual : FC -> List PDecl -> PDecl
PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl
PNamespace : FC -> List String -> List PDecl -> PDecl
PTransform : FC -> PTerm -> PTerm -> PDecl
PDirective : FC -> Directive -> PDecl
definedInData : PDataDecl -> List Name

1
src/TTImp/Elab.idr
View File

@ -6,6 +6,7 @@ import Core.Env
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Transform
import Core.UnifyState
import Core.Unify

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

@ -369,7 +369,7 @@ mutual
tm x aty sc arg expargs impargs kr expty
-- Function type is delayed, so force the term and continue
checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _) sc)) expargs impargs kr expty
= checkAppWith rig elabinfo nest env fc (TForce dfc tm) ty expargs impargs kr expty
= checkAppWith rig elabinfo nest env fc (TForce dfc r tm) ty expargs impargs kr expty
-- If there's no more arguments given, and the plicities of the type and
-- the expected type line up, stop
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi rigb Implicit aty) sc)

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

@ -37,8 +37,8 @@ changeVar old new (TDelayed fc r p)
= TDelayed fc r (changeVar old new p)
changeVar old new (TDelay fc r t p)
= TDelay fc r (changeVar old new t) (changeVar old new p)
changeVar old new (TForce fc p)
= TForce fc (changeVar old new p)
changeVar old new (TForce fc r p)
= TForce fc r (changeVar old new p)
changeVar old new tm = tm
findLater : (x : Name) -> (newer : List Name) -> Var (newer ++ x :: older)
@ -342,19 +342,20 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
canBindName _ vs = Nothing
addEnv : Env Term vs -> SubVars vs' vs -> List Name ->
(List (Maybe RawImp), List Name)
addEnv [] sub used = ([], used)
List (Maybe RawImp)
addEnv [] sub used = []
addEnv {vs = v :: vs} (b :: bs) SubRefl used
= let (rest, used') = addEnv bs SubRefl used in
(Nothing :: rest, used')
= let rest = addEnv bs SubRefl used in
Nothing :: rest
addEnv (b :: bs) (KeepCons p) used
= let (rest, used') = addEnv bs p used in
(Nothing :: rest, used')
= let rest = addEnv bs p used in
Nothing :: rest
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 UseLeft n (Implicit fc True)) :: rest, n :: used')
_ => (Just (Implicit fc True) :: rest, used')
= case canBindName v used of
Just n => let rest = addEnv bs p (n :: used) in
Just (IAs fc UseLeft n (Implicit fc True)) :: rest
_ => let rest = addEnv bs p used in
Just (Implicit fc True) :: rest
-- Replace a variable in the argument list; if the reference is to
-- a variable kept in the outer environment (therefore not an argument
@ -393,16 +394,16 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
Env Term vars -> SubVars vs' vars ->
ImpClause -> ImpClause
updateClause casen splitOn env sub (PatClause loc' lhs rhs)
= let args = fst (addEnv env sub (usedIn lhs))
= let args = addEnv env sub (usedIn lhs)
args' = mkSplit splitOn lhs args in
PatClause loc' (apply (IVar loc' casen) args') rhs
-- With isn't allowed in a case block but include for completeness
updateClause casen splitOn env sub (WithClause loc' lhs wval cs)
= let args = fst (addEnv env sub (usedIn lhs))
= let args = addEnv env sub (usedIn lhs)
args' = mkSplit splitOn lhs args in
WithClause loc' (apply (IVar loc' casen) args') wval cs
updateClause casen splitOn env sub (ImpossibleClause loc' lhs)
= let args = fst (addEnv env sub (usedIn lhs))
= let args = addEnv env sub (usedIn lhs)
args' = mkSplit splitOn lhs args in
ImpossibleClause loc' (apply (IVar loc' casen) args')

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

@ -588,10 +588,10 @@ checkExp rig elabinfo env fc tm got (Just exp)
[] => case addLazy vs of
NoLazy => do logTerm 5 "Solved" tm
pure (tm, got)
AddForce => do logTerm 5 "Force" tm
logGlue 5 "Got" env got
logGlue 5 "Exp" env exp
pure (TForce fc tm, exp)
AddForce r => do logTerm 5 "Force" tm
logGlue 5 "Got" env got
logGlue 5 "Exp" env exp
pure (TForce fc r tm, exp)
AddDelay r => do ty <- getTerm got
logTerm 5 "Delay" tm
pure (TDelay fc r ty tm, exp)
@ -603,7 +603,7 @@ checkExp rig elabinfo env fc tm got (Just exp)
dumpConstraints 5 False
case addLazy vs of
NoLazy => pure (ctm, got)
AddForce => pure (TForce fc tm, got)
AddForce r => pure (TForce fc r tm, got)
AddDelay r => do ty <- getTerm got
pure (TDelay fc r ty tm, got)
checkExp rig elabinfo env fc tm got Nothing = pure (tm, got)

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

@ -47,7 +47,7 @@ mutual
embedSub sub (TDelayed fc x y) = TDelayed fc x (embedSub sub y)
embedSub sub (TDelay fc x t y)
= TDelay fc x (embedSub sub t) (embedSub sub y)
embedSub sub (TForce fc x) = TForce fc (embedSub sub x)
embedSub sub (TForce fc r x) = TForce fc r (embedSub sub x)
embedSub sub (PrimVal fc c) = PrimVal fc c
embedSub sub (Erased fc) = Erased fc
embedSub sub (TType fc) = TType fc
@ -202,7 +202,7 @@ swapVars (App fc fn arg) = App fc (swapVars fn) (swapVars arg)
swapVars (As fc nm pat) = As fc (swapVars nm) (swapVars pat)
swapVars (TDelayed fc x tm) = TDelayed fc x (swapVars tm)
swapVars (TDelay fc x ty tm) = TDelay fc x (swapVars ty) (swapVars tm)
swapVars (TForce fc tm) = TForce fc (swapVars tm)
swapVars (TForce fc r tm) = TForce fc r (swapVars tm)
swapVars (PrimVal fc c) = PrimVal fc c
swapVars (Erased fc) = Erased fc
swapVars (TType fc) = TType fc

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

@ -87,6 +87,6 @@ checkForce rig elabinfo nest env fc tm exp
(tm', gty) <- check rig elabinfo nest env tm expf
tynf <- getNF gty
case tynf of
NDelayed _ _ expnf =>
pure (TForce fc tm', glueBack defs env expnf)
NDelayed _ r expnf =>
pure (TForce fc r tm', glueBack defs env expnf)
_ => throw (GenericMsg fc "Forcing a non-delayed type")

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

@ -5,6 +5,7 @@ import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value
@ -23,6 +24,7 @@ import TTImp.Elab.Local
import TTImp.Elab.Prim
import TTImp.Elab.Record
import TTImp.Elab.Rewrite
import TTImp.Reflect
import TTImp.TTImp
%default covering
@ -49,7 +51,7 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamTm tm exp
= case getFn exp of
Ref _ Func _ => pure Nothing -- might still be implicit
TForce _ _ => pure Nothing
TForce _ _ _ => pure Nothing
Bind _ _ (Lam _ _ _) _ => pure Nothing
_ => pure $ Just tm

2
src/TTImp/Interactive/MakeLemma.idr
View File

@ -28,7 +28,7 @@ bindable p tm
(Ref _ (DataCon _ _) _, args) => any (bindable p) args
(TDelayed _ _ t, args) => any (bindable p) (t :: args)
(TDelay _ _ _ t, args) => any (bindable p) (t :: args)
(TForce _ t, args) => any (bindable p) (t :: args)
(TForce _ _ t, args) => any (bindable p) (t :: args)
(Local _ _ p' _, []) => p == p'
_ => False

2
src/TTImp/ProcessDecls.idr
View File

@ -46,6 +46,8 @@ process eopts nest env (INamespace fc nested ns decls)
nestedNS = if nested
then newns :: nns
else nns } defs)
process eopts nest env (ITransform fc lhs rhs)
= throw (GenericMsg fc "%transform not yet implemented")
process {c} eopts nest env (IPragma act)
= act c nest env
process eopts nest env (ILog n)

623
src/TTImp/Reflect.idr Normal file
View File

@ -0,0 +1,623 @@
module TTImp.Reflect
import Core.Context
import Core.Env
import Core.Normalise
import Core.Reflect
import Core.TT
import Core.Value
import TTImp.TTImp
%default covering
export
Reify BindMode where
reify defs (NDCon _ (NS _ (UN "PI")) _ _ [c])
= do c' <- reify defs !(evalClosure defs c)
pure (PI c')
reify defs (NDCon _ (NS _ (UN "PATTERN")) _ _ _)
= pure PATTERN
reify defs (NDCon _ (NS _ (UN "NONE")) _ _ _)
= pure NONE
reify deva val = cantReify val "BindMode"
export
Reflect BindMode where
reflect fc defs env (PI c)
= do c' <- reflect fc defs env c
appCon fc defs (reflection "PI") [c']
reflect fc defs env PATTERN
= getCon fc defs (reflection "PATTERN")
reflect fc defs env NONE
= getCon fc defs (reflection "NONE")
export
Reify UseSide where
reify defs (NDCon _ (NS _ (UN "UseLeft")) _ _ _)
= pure UseLeft
reify defs (NDCon _ (NS _ (UN "UseRight")) _ _ _)
= pure UseRight
reify deva val = cantReify val "UseSide"
export
Reflect UseSide where
reflect fc defs env UseLeft
= getCon fc defs (reflection "UseLeft")
reflect fc defs env UseRight
= getCon fc defs (reflection "UseRight")
mutual
export
Reify RawImp where
reify defs (NDCon _ (NS _ (UN "IVar")) _ _ [fc, n])
= do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n)
pure (IVar fc' n')
reify defs (NDCon _ (NS _ (UN "IPi")) _ _ [fc, c, p, mn, aty, rty])
= do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c)
p' <- reify defs !(evalClosure defs p)
mn' <- reify defs !(evalClosure defs mn)
aty' <- reify defs !(evalClosure defs aty)
rty' <- reify defs !(evalClosure defs rty)
pure (IPi fc' c' p' mn' aty' rty')
reify defs (NDCon _ (NS _ (UN "ILam")) _ _ [fc, c, p, mn, aty, lty])
= do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c)
p' <- reify defs !(evalClosure defs p)
mn' <- reify defs !(evalClosure defs mn)
aty' <- reify defs !(evalClosure defs aty)
lty' <- reify defs !(evalClosure defs lty)
pure (ILam fc' c' p' mn' aty' lty')
reify defs (NDCon _ (NS _ (UN "ILet")) _ _ [fc, c, n, ty, val, sc])
= do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c)
n' <- reify defs !(evalClosure defs n)
ty' <- reify defs !(evalClosure defs ty)
val' <- reify defs !(evalClosure defs val)
sc' <- reify defs !(evalClosure defs sc)
pure (ILet fc' c' n' ty' val' sc')
reify defs (NDCon _ (NS _ (UN "ICase")) _ _ [fc, sc, ty, cs])
= do fc' <- reify defs !(evalClosure defs fc)
sc' <- reify defs !(evalClosure defs sc)
ty' <- reify defs !(evalClosure defs ty)
cs' <- reify defs !(evalClosure defs cs)
pure (ICase fc' sc' ty' cs')
reify defs (NDCon _ (NS _ (UN "ILocal")) _ _ [fc, ds, sc])
= do fc' <- reify defs !(evalClosure defs fc)
ds' <- reify defs !(evalClosure defs ds)
sc' <- reify defs !(evalClosure defs sc)
pure (ILocal fc' ds' sc')
reify defs (NDCon _ (NS _ (UN "IUpdate")) _ _ [fc, ds, sc])
= do fc' <- reify defs !(evalClosure defs fc)
ds' <- reify defs !(evalClosure defs ds)
sc' <- reify defs !(evalClosure defs sc)
pure (IUpdate fc' ds' sc')
reify defs (NDCon _ (NS _ (UN "IApp")) _ _ [fc, f, a])
= do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a)
pure (IApp fc' f' a')
reify defs (NDCon _ (NS _ (UN "IImplicitApp")) _ _ [fc, f, m, a])
= do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
m' <- reify defs !(evalClosure defs m)
a' <- reify defs !(evalClosure defs a)
pure (IImplicitApp fc' f' m' a')
reify defs (NDCon _ (NS _ (UN "IWithApp")) _ _ [fc, f, a])
= do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a)
pure (IWithApp fc' f' a')
reify defs (NDCon _ (NS _ (UN "ISearch")) _ _ [fc, d])
= do fc' <- reify defs !(evalClosure defs fc)
d' <- reify defs !(evalClosure defs d)
pure (ISearch fc' d')
reify defs (NDCon _ (NS _ (UN "IAlternative")) _ _ [fc, t, as])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
as' <- reify defs !(evalClosure defs as)
pure (IAlternative fc' t' as')
reify defs (NDCon _ (NS _ (UN "IRewrite")) _ _ [fc, t, sc])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
sc' <- reify defs !(evalClosure defs sc)
pure (IRewrite fc' t' sc')
reify defs (NDCon _ (NS _ (UN "IBindHere")) _ _ [fc, t, sc])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
sc' <- reify defs !(evalClosure defs sc)
pure (IBindHere fc' t' sc')
reify defs (NDCon _ (NS _ (UN "IBindVar")) _ _ [fc, n])
= do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n)
pure (IBindVar fc' n')
reify defs (NDCon _ (NS _ (UN "IAs")) _ _ [fc, s, n, t])
= do fc' <- reify defs !(evalClosure defs fc)
s' <- reify defs !(evalClosure defs s)
n' <- reify defs !(evalClosure defs n)
t' <- reify defs !(evalClosure defs t)
pure (IAs fc' s' n' t')
reify defs (NDCon _ (NS _ (UN "IMustUnify")) _ _ [fc, r, t])
= do fc' <- reify defs !(evalClosure defs fc)
r' <- reify defs !(evalClosure defs r)
t' <- reify defs !(evalClosure defs t)
pure (IMustUnify fc' r' t')
reify defs (NDCon _ (NS _ (UN "IDelayed")) _ _ [fc, r, t])
= do fc' <- reify defs !(evalClosure defs fc)
r' <- reify defs !(evalClosure defs r)
t' <- reify defs !(evalClosure defs t)
pure (IDelayed fc' r' t')
reify defs (NDCon _ (NS _ (UN "IDelay")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IDelay fc' t')
reify defs (NDCon _ (NS _ (UN "IForce")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IForce fc' t')
reify defs (NDCon _ (NS _ (UN "IPrimVal")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IPrimVal fc' t')
reify defs (NDCon _ (NS _ (UN "IType")) _ _ [fc])
= do fc' <- reify defs !(evalClosure defs fc)
pure (IType fc')
reify defs (NDCon _ (NS _ (UN "IHole")) _ _ [fc, n])
= do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n)
pure (IHole fc' n')
reify defs (NDCon _ (NS _ (UN "Implicit")) _ _ [fc, n])
= do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n)
pure (Implicit fc' n')
reify defs val = cantReify val "TTImp"
export
Reify IFieldUpdate where
reify defs (NDCon _ (NS _ (UN "ISetField")) _ _ [x, y])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
pure (ISetField x' y')
reify defs (NDCon _ (NS _ (UN "ISetFieldApp")) _ _ [x, y])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
pure (ISetFieldApp x' y')
reify defs val = cantReify val "IFieldUpdate"
export
Reify AltType where
reify defs (NDCon _ (NS _ (UN "FirstSuccess")) _ _ _)
= pure FirstSuccess
reify defs (NDCon _ (NS _ (UN "Unique")) _ _ _)
= pure Unique
reify defs (NDCon _ (NS _ (UN "UniqueDefault")) _ _ [x])
= do x' <- reify defs !(evalClosure defs x)
pure (UniqueDefault x')
reify defs val = cantReify val "AltType"
export
Reify FnOpt where
reify defs (NDCon _ (NS _ (UN "Inline")) _ _ _)
= pure Inline
reify defs (NDCon _ (NS _ (UN "Hint")) _ _ [x])
= do x' <- reify defs !(evalClosure defs x)
pure (Hint x')
reify defs (NDCon _ (NS _ (UN "GlobalHint")) _ _ [x])
= do x' <- reify defs !(evalClosure defs x)
pure (GlobalHint x')
reify defs (NDCon _ (NS _ (UN "ExternFn")) _ _ _)
= pure ExternFn
reify defs (NDCon _ (NS _ (UN "ForeignFn")) _ _ [x])
= do x' <- reify defs !(evalClosure defs x)
pure (ForeignFn x')
reify defs (NDCon _ (NS _ (UN "Invertible")) _ _ _)
= pure Invertible
reify defs (NDCon _ (NS _ (UN "Total")) _ _ _)
= pure Total
reify defs (NDCon _ (NS _ (UN "Covering")) _ _ _)
= pure Covering
reify defs (NDCon _ (NS _ (UN "PartialOK")) _ _ _)
= pure PartialOK
reify defs val = cantReify val "FnOpt"
export
Reify ImpTy where
reify defs (NDCon _ (NS _ (UN "MkTy")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (MkImpTy x' y' z')
reify defs val = cantReify val "ITy"
export
Reify DataOpt where
reify defs (NDCon _ (NS _ (UN "SearchBy")) _ _ [x])
= do x' <- reify defs !(evalClosure defs x)
pure (SearchBy x')
reify defs (NDCon _ (NS _ (UN "NoHints")) _ _ _)
= pure NoHints
reify defs val = cantReify val "DataOpt"
export
Reify ImpData where
reify defs (NDCon _ (NS _ (UN "MkData")) _ _ [v,w,x,y,z])
= do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (MkImpData v' w' x' y' z')
reify defs (NDCon _ (NS _ (UN "MkLater")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (MkImpLater x' y' z')
reify defs val = cantReify val "Data"
export
Reify IField where
reify defs (NDCon _ (NS _ (UN "MkIField")) _ _ [v,w,x,y,z])
= do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (MkIField v' w' x' y' z')
reify defs val = cantReify val "IField"
export
Reify ImpRecord where
reify defs (NDCon _ (NS _ (UN "MkRecord")) _ _ [v,w,x,y,z])
= do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (MkImpRecord v' w' x' y' z')
reify defs val = cantReify val "Record"
export
Reify ImpClause where
reify defs (NDCon _ (NS _ (UN "PatClause")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (PatClause x' y' z')
reify defs (NDCon _ (NS _ (UN "WithClause")) _ _ [w,x,y,z])
= do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (WithClause w' x' y' z')
reify defs (NDCon _ (NS _ (UN "WithClause")) _ _ [x,y])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
pure (ImpossibleClause x' y')
reify defs val = cantReify val "Clause"
export
Reify ImpDecl where
reify defs (NDCon _ (NS _ (UN "IClaim")) _ _ [v,w,x,y,z])
= do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (IClaim v' w' x' y' z')
reify defs (NDCon _ (NS _ (UN "IData")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (IData x' y' z')
reify defs (NDCon _ (NS _ (UN "IDef")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (IDef x' y' z')
reify defs (NDCon _ (NS _ (UN "IParameters")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (IParameters x' y' z')
reify defs (NDCon _ (NS _ (UN "IRecord")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (IRecord x' y' z')
reify defs (NDCon _ (NS _ (UN "INamespace")) _ _ [w,x,y,z])
= do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (INamespace w' x' y' z')
reify defs (NDCon _ (NS _ (UN "ITransform")) _ _ [x,y,z])
= do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z)
pure (ITransform x' y' z')
reify defs (NDCon _ (NS _ (UN "ILog")) _ _ [x])
= do x' <- reify defs !(evalClosure defs x)
pure (ILog x')
reify defs val = cantReify val "Decl"
mutual
export
Reflect RawImp where
reflect fc defs env (IVar tfc n)
= do fc' <- reflect fc defs env tfc
n' <- reflect fc defs env n
appCon fc defs (reflection "IVar") [fc', n']
reflect fc defs env (IPi tfc c p mn aty rty)
= do fc' <- reflect fc defs env tfc
c' <- reflect fc defs env c
p' <- reflect fc defs env p
mn' <- reflect fc defs env mn
aty' <- reflect fc defs env aty
rty' <- reflect fc defs env rty
appCon fc defs (reflection "IPi") [fc', c', p', mn', aty', rty']
reflect fc defs env (ILam tfc c p mn aty rty)
= do fc' <- reflect fc defs env tfc
c' <- reflect fc defs env c
p' <- reflect fc defs env p
mn' <- reflect fc defs env mn
aty' <- reflect fc defs env aty
rty' <- reflect fc defs env rty
appCon fc defs (reflection "ILam") [fc', c', p', mn', aty', rty']
reflect fc defs env (ILet tfc c n aty aval sc)
= do fc' <- reflect fc defs env tfc
c' <- reflect fc defs env c
n' <- reflect fc defs env n
aty' <- reflect fc defs env aty
aval' <- reflect fc defs env aval
sc' <- reflect fc defs env sc
appCon fc defs (reflection "ILet") [fc', c', n', aty', aval', sc']
reflect fc defs env (ICase tfc sc ty cs)
= do fc' <- reflect fc defs env tfc
sc' <- reflect fc defs env sc
ty' <- reflect fc defs env ty
cs' <- reflect fc defs env cs
appCon fc defs (reflection "ICase") [fc', sc', ty', cs']
reflect fc defs env (ILocal tfc ds sc)
= do fc' <- reflect fc defs env tfc
ds' <- reflect fc defs env ds
sc' <- reflect fc defs env sc
appCon fc defs (reflection "ILocal") [fc', ds', sc']
reflect fc defs env (IUpdate tfc ds sc)
= do fc' <- reflect fc defs env tfc
ds' <- reflect fc defs env ds
sc' <- reflect fc defs env sc
appCon fc defs (reflection "IUpdate") [fc', ds', sc']
reflect fc defs env (IApp tfc f a)
= do fc' <- reflect fc defs env tfc
f' <- reflect fc defs env f
a' <- reflect fc defs env a
appCon fc defs (reflection "IApp") [fc', f', a']
reflect fc defs env (IImplicitApp tfc f m a)
= do fc' <- reflect fc defs env tfc
f' <- reflect fc defs env f
m' <- reflect fc defs env m
a' <- reflect fc defs env a
appCon fc defs (reflection "IImplicitApp") [fc', f', m', a']
reflect fc defs env (IWithApp tfc f a)
= do fc' <- reflect fc defs env tfc
f' <- reflect fc defs env f
a' <- reflect fc defs env a
appCon fc defs (reflection "IWithApp") [fc', f', a']
reflect fc defs env (ISearch tfc d)
= do fc' <- reflect fc defs env tfc
d' <- reflect fc defs env d
appCon fc defs (reflection "ISearch") [fc', d']
reflect fc defs env (IAlternative tfc t as)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
as' <- reflect fc defs env as
appCon fc defs (reflection "IAlternative") [fc', t', as']
reflect fc defs env (IRewrite tfc t sc)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
sc' <- reflect fc defs env sc
appCon fc defs (reflection "IRewrite") [fc', t', sc']
reflect fc defs env (ICoerced tfc d) = reflect fc defs env d
reflect fc defs env (IBindHere tfc n sc)
= do fc' <- reflect fc defs env tfc
n' <- reflect fc defs env n
sc' <- reflect fc defs env sc
appCon fc defs (reflection "IBindHere") [fc', n', sc']
reflect fc defs env (IBindVar tfc n)
= do fc' <- reflect fc defs env tfc
n' <- reflect fc defs env n
appCon fc defs (reflection "IBindVar") [fc', n']
reflect fc defs env (IAs tfc s n t)
= do fc' <- reflect fc defs env tfc
s' <- reflect fc defs env s
n' <- reflect fc defs env n
t' <- reflect fc defs env t
appCon fc defs (reflection "IAs") [fc', s', n', t']
reflect fc defs env (IMustUnify tfc r t)
= do fc' <- reflect fc defs env tfc
r' <- reflect fc defs env r
t' <- reflect fc defs env t
appCon fc defs (reflection "IMustUnify") [fc', r', t']
reflect fc defs env (IDelayed tfc r t)
= do fc' <- reflect fc defs env tfc
r' <- reflect fc defs env r
t' <- reflect fc defs env t
appCon fc defs (reflection "IDelayed") [fc', r', t']
reflect fc defs env (IDelay tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflection "IDelay") [fc', t']
reflect fc defs env (IForce tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflection "IForce") [fc', t']
reflect fc defs env (IPrimVal tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflection "IPrimVal") [fc', t']
reflect fc defs env (IType tfc)
= do fc' <- reflect fc defs env tfc
appCon fc defs (reflection "IType") [fc']
reflect fc defs env (IHole tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflection "IHole") [fc', t']
reflect fc defs env (Implicit tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflection "Implicit") [fc', t']
export
Reflect IFieldUpdate where
reflect fc defs env (ISetField p t)
= do p' <- reflect fc defs env p
t' <- reflect fc defs env t
appCon fc defs (reflection "ISetField") [p', t']
reflect fc defs env (ISetFieldApp p t)
= do p' <- reflect fc defs env p
t' <- reflect fc defs env t
appCon fc defs (reflection "ISetFieldApp") [p', t']
export
Reflect AltType where
reflect fc defs env FirstSuccess = getCon fc defs (reflection "FirstSuccess")
reflect fc defs env Unique = getCon fc defs (reflection "Unique")
reflect fc defs env (UniqueDefault x)
= do x' <- reflect fc defs env x
appCon fc defs (reflection "UniqueDefault") [x']
export
Reflect FnOpt where
reflect fc defs env Inline = getCon fc defs (reflection "FirstSuccess")
reflect fc defs env (Hint x)
= do x' <- reflect fc defs env x
appCon fc defs (reflection "Hint") [x']
reflect fc defs env (GlobalHint x)
= do x' <- reflect fc defs env x
appCon fc defs (reflection "GlobalHint") [x']
reflect fc defs env ExternFn = getCon fc defs (reflection "ExternFn")
reflect fc defs env (ForeignFn x)
= do x' <- reflect fc defs env x
appCon fc defs (reflection "ForeignFn") [x']
reflect fc defs env Invertible = getCon fc defs (reflection "Invertible")
reflect fc defs env Total = getCon fc defs (reflection "Total")
reflect fc defs env Covering = getCon fc defs (reflection "Covering")
reflect fc defs env PartialOK = getCon fc defs (reflection "PartialOK")
export
Reflect ImpTy where
reflect fc defs env (MkImpTy x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "MkTy") [x', y', z']
export
Reflect DataOpt where
reflect fc defs env (SearchBy x)
= do x' <- reflect fc defs env x
appCon fc defs (reflection "SearchBy") [x']
reflect fc defs env NoHints = getCon fc defs (reflection "NoHints")
export
Reflect ImpData where
reflect fc defs env (MkImpData v w x y z)
= do v' <- reflect fc defs env v
w' <- reflect fc defs env w
x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "MkData") [v', w', x', y', z']
reflect fc defs env (MkImpLater x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "MkLater") [x', y', z']
export
Reflect IField where
reflect fc defs env (MkIField v w x y z)
= do v' <- reflect fc defs env v
w' <- reflect fc defs env w
x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "MkIField") [v', w', x', y', z']
export
Reflect ImpRecord where
reflect fc defs env (MkImpRecord v w x y z)
= do v' <- reflect fc defs env v
w' <- reflect fc defs env w
x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "MkRecord") [v', w', x', y', z']
export
Reflect ImpClause where
reflect fc defs env (PatClause x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "PatClause") [x', y', z']
reflect fc defs env (WithClause w x y z)
= do w' <- reflect fc defs env x
x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "WithClause") [w', x', y', z']
reflect fc defs env (ImpossibleClause x y)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
appCon fc defs (reflection "ImpossibleClause") [x', y']
export
Reflect ImpDecl where
reflect fc defs env (IClaim v w x y z)
= do v' <- reflect fc defs env v
w' <- reflect fc defs env w
x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "IClaim") [v', w', x', y', z']
reflect fc defs env (IData x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "IData") [x', y', z']
reflect fc defs env (IDef x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "IDef") [x', y', z']
reflect fc defs env (IParameters x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "IParameters") [x', y', z']
reflect fc defs env (IRecord x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "IRecord") [x', y', z']
reflect fc defs env (INamespace w x y z)
= do w' <- reflect fc defs env w
x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "INamespace") [w', x', y', z']
reflect fc defs env (ITransform x y z)
= do x' <- reflect fc defs env x
y' <- reflect fc defs env y
z' <- reflect fc defs env z
appCon fc defs (reflection "ITransform") [x', y', z']
reflect fc defs env (IPragma x)
= throw (GenericMsg fc "Can't reflect a pragma")
reflect fc defs env (ILog x)
= do x' <- reflect fc defs env x
appCon fc defs (reflection "ILog") [x']

11
src/TTImp/TTImp.idr
View File

@ -285,6 +285,7 @@ mutual
-- ^ if True, parent namespaces in the same file can also
-- look inside and see private/export names in full
List String -> List ImpDecl -> ImpDecl
ITransform : FC -> RawImp -> RawImp -> ImpDecl
IPragma : ({vars : _} -> Ref Ctxt Defs ->
NestedNames vars -> Env Term vars -> Core ()) ->
ImpDecl
@ -302,6 +303,8 @@ mutual
show (INamespace _ nest ns decls)
= "namespace " ++ if nest then "[nested] " else "" ++ show ns ++
showSep "\n" (assert_total $ map show decls)
show (ITransform _ lhs rhs)
= "%transform " ++ show lhs ++ " ==> " ++ show rhs
show (IPragma _) = "[externally defined pragma]"
show (ILog lvl) = "%logging " ++ show lvl
@ -836,9 +839,11 @@ mutual
= do tag 4; toBuf b fc; toBuf b vis; toBuf b r
toBuf b (INamespace fc n xs ds)
= do tag 5; toBuf b fc; toBuf b n; toBuf b xs; toBuf b ds
toBuf b (ITransform fc lhs rhs)
= do tag 6; toBuf b fc; toBuf b lhs; toBuf b rhs
toBuf b (IPragma f) = throw (InternalError "Can't write Pragma")
toBuf b (ILog n)
= do tag 6; toBuf b n
= do tag 7; toBuf b n
fromBuf b
= case !getTag of
@ -861,7 +866,9 @@ mutual
5 => do fc <- fromBuf b; n <- fromBuf b; xs <- fromBuf b
ds <- fromBuf b
pure (INamespace fc n xs ds)
6 => do n <- fromBuf b
6 => do fc <- fromBuf b; lhs <- fromBuf b; rhs <- fromBuf b
pure (ITransform fc lhs rhs)
7 => do n <- fromBuf b
pure (ILog n)
_ => corrupt "ImpDecl"

4
src/TTImp/Unelab.idr
View File

@ -23,7 +23,7 @@ used idx (App _ f a) = used idx f || used idx a
used idx (As _ _ pat) = used idx pat
used idx (TDelayed _ _ tm) = used idx tm
used idx (TDelay _ _ _ tm) = used idx tm
used idx (TForce _ tm) = used idx tm
used idx (TForce _ _ tm) = used idx tm
used idx _ = False
data IArg
@ -176,7 +176,7 @@ mutual
= do (tm', ty) <- unelabTy' umode env tm
defs <- get Ctxt
pure (IDelay fc tm', gErased fc)
unelabTy' umode env (TForce fc tm)
unelabTy' umode env (TForce fc r tm)
= do (tm', ty) <- unelabTy' umode env tm
defs <- get Ctxt
pure (IForce fc tm', gErased fc)