mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 22:06:33 +03:00
Make 'with' work in where blocks
Need to set up nested names appropriately for the with function so that the environment gets passed through correctly, and use abstractEnvType to get the type of the with function rather than simply binding the environment as is.
This commit is contained in:
parent
1cc097aefc
commit
11560a5c82
@ -35,52 +35,52 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
|
|||||||
traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
|
traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
|
||||||
check rig elabinfo nest' env scope expty
|
check rig elabinfo nest' env scope expty
|
||||||
where
|
where
|
||||||
-- For the local definitions, don't allow access to linear things
|
-- For the local definitions, don't allow access to linear things
|
||||||
-- unless they're explicitly passed.
|
-- unless they're explicitly passed.
|
||||||
-- This is because, at the moment, we don't have any mechanism of
|
-- This is because, at the moment, we don't have any mechanism of
|
||||||
-- ensuring the nested definition is used exactly once
|
-- ensuring the nested definition is used exactly once
|
||||||
dropLinear : Env Term vs -> Env Term vs
|
dropLinear : Env Term vs -> Env Term vs
|
||||||
dropLinear [] = []
|
dropLinear [] = []
|
||||||
dropLinear (b :: bs)
|
dropLinear (b :: bs)
|
||||||
= if isLinear (multiplicity b)
|
= if isLinear (multiplicity b)
|
||||||
then setMultiplicity b Rig0 :: dropLinear bs
|
then setMultiplicity b Rig0 :: dropLinear bs
|
||||||
else b :: dropLinear bs
|
else b :: dropLinear bs
|
||||||
|
|
||||||
applyEnv : Int -> Name ->
|
applyEnv : Int -> Name ->
|
||||||
Core (Name, (Maybe Name, FC -> NameType -> Term vars))
|
Core (Name, (Maybe Name, FC -> NameType -> Term vars))
|
||||||
applyEnv outer inner
|
applyEnv outer inner
|
||||||
= do n' <- resolveName (Nested outer inner)
|
= do n' <- resolveName (Nested outer inner)
|
||||||
pure (inner, (Just (Nested outer inner),
|
pure (inner, (Just (Nested outer inner),
|
||||||
\fc, nt => applyTo fc
|
\fc, nt => applyTo fc
|
||||||
(Ref fc nt (Resolved n')) env))
|
(Ref fc nt (Resolved n')) env))
|
||||||
|
|
||||||
-- Update the names in the declarations to the new 'nested' names.
|
-- Update the names in the declarations to the new 'nested' names.
|
||||||
-- When we encounter the names in elaboration, we'll update to an
|
-- When we encounter the names in elaboration, we'll update to an
|
||||||
-- application of the nested name.
|
-- application of the nested name.
|
||||||
newName : NestedNames vars -> Name -> Name
|
newName : NestedNames vars -> Name -> Name
|
||||||
newName nest n
|
newName nest n
|
||||||
= case lookup n (names nest) of
|
= case lookup n (names nest) of
|
||||||
Just (Just n', _) => n'
|
Just (Just n', _) => n'
|
||||||
_ => n
|
_ => n
|
||||||
|
|
||||||
updateTyName : NestedNames vars -> ImpTy -> ImpTy
|
updateTyName : NestedNames vars -> ImpTy -> ImpTy
|
||||||
updateTyName nest (MkImpTy loc' n ty)
|
updateTyName nest (MkImpTy loc' n ty)
|
||||||
= MkImpTy loc' (newName nest n) ty
|
= MkImpTy loc' (newName nest n) ty
|
||||||
|
|
||||||
updateDataName : NestedNames vars -> ImpData -> ImpData
|
updateDataName : NestedNames vars -> ImpData -> ImpData
|
||||||
updateDataName nest (MkImpData loc' n tycons dopts dcons)
|
updateDataName nest (MkImpData loc' n tycons dopts dcons)
|
||||||
= MkImpData loc' (newName nest n) tycons dopts
|
= MkImpData loc' (newName nest n) tycons dopts
|
||||||
(map (updateTyName nest) dcons)
|
(map (updateTyName nest) dcons)
|
||||||
updateDataName nest (MkImpLater loc' n tycons)
|
updateDataName nest (MkImpLater loc' n tycons)
|
||||||
= MkImpLater loc' (newName nest n) tycons
|
= MkImpLater loc' (newName nest n) tycons
|
||||||
|
|
||||||
updateName : NestedNames vars -> ImpDecl -> ImpDecl
|
updateName : NestedNames vars -> ImpDecl -> ImpDecl
|
||||||
updateName nest (IClaim loc' r vis fnopts ty)
|
updateName nest (IClaim loc' r vis fnopts ty)
|
||||||
= IClaim loc' r vis fnopts (updateTyName nest ty)
|
= IClaim loc' r vis fnopts (updateTyName nest ty)
|
||||||
updateName nest (IDef loc' n cs)
|
updateName nest (IDef loc' n cs)
|
||||||
= IDef loc' (newName nest n) cs
|
= IDef loc' (newName nest n) cs
|
||||||
updateName nest (IData loc' vis d)
|
updateName nest (IData loc' vis d)
|
||||||
= IData loc' vis (updateDataName nest d)
|
= IData loc' vis (updateDataName nest d)
|
||||||
updateName nest i = i
|
updateName nest i = i
|
||||||
|
|
||||||
|
|
||||||
|
@ -256,7 +256,8 @@ plicit (Pi _ p _) = p
|
|||||||
plicit (PVar _ p _) = p
|
plicit (PVar _ p _) = p
|
||||||
plicit _ = Explicit
|
plicit _ = Explicit
|
||||||
|
|
||||||
bindNotReq : FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
|
bindNotReq : {vs : _} ->
|
||||||
|
FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
|
||||||
List (PiInfo, Name) ->
|
List (PiInfo, Name) ->
|
||||||
Term vs -> (List (PiInfo, Name), Term pre)
|
Term vs -> (List (PiInfo, Name), Term pre)
|
||||||
bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
|
bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
|
||||||
@ -272,14 +273,16 @@ bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
|
|||||||
= bindNotReq fc i env p ((plicit b, n) :: ns)
|
= bindNotReq fc i env p ((plicit b, n) :: ns)
|
||||||
(Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm)
|
(Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm)
|
||||||
|
|
||||||
bindReq : FC -> Env Term vs -> (sub : SubVars pre vs) ->
|
bindReq : {vs : _} ->
|
||||||
|
FC -> Env Term vs -> (sub : SubVars pre vs) ->
|
||||||
List (PiInfo, Name) ->
|
List (PiInfo, Name) ->
|
||||||
Term pre -> Maybe (List (PiInfo, Name), ClosedTerm)
|
Term pre -> Maybe (List (PiInfo, Name), List Name, ClosedTerm)
|
||||||
bindReq fc env SubRefl ns tm = pure (ns, bindEnv fc env tm)
|
bindReq {vs} fc env SubRefl ns tm
|
||||||
bindReq fc {vs = n :: _} (b :: env) (KeepCons p) ns tm
|
= pure (ns, reverse vs, abstractEnvType fc env tm)
|
||||||
= do b' <- shrinkBinder b p
|
bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
|
||||||
bindReq fc env p ((plicit b, n) :: ns)
|
= do b' <- shrinkBinder b p
|
||||||
(Bind fc _ (Pi (multiplicity b) Explicit (binderType b')) tm)
|
bindReq fc env p ((plicit b, n) :: ns)
|
||||||
|
(Bind fc _ (Pi (multiplicity b) Explicit (binderType b')) tm)
|
||||||
bindReq fc (b :: env) (DropCons p) ns tm
|
bindReq fc (b :: env) (DropCons p) ns tm
|
||||||
= bindReq fc env p ns tm
|
= bindReq fc env p ns tm
|
||||||
|
|
||||||
@ -397,6 +400,16 @@ withRHS fc drop wname wargnames tm toplhs
|
|||||||
wrhsC : ImpClause -> Core ImpClause
|
wrhsC : ImpClause -> Core ImpClause
|
||||||
wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)
|
wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)
|
||||||
wrhsC c = pure c
|
wrhsC c = pure c
|
||||||
|
|
||||||
|
-- For checking with blocks as nested names
|
||||||
|
applyEnv : {auto c : Ref Ctxt Defs} ->
|
||||||
|
Env Term vars -> Name ->
|
||||||
|
Core (Name, (Maybe Name, FC -> NameType -> Term vars))
|
||||||
|
applyEnv env withname
|
||||||
|
= do n' <- resolveName withname
|
||||||
|
pure (withname, (Just withname,
|
||||||
|
\fc, nt => applyTo fc
|
||||||
|
(Ref fc nt (Resolved n')) env))
|
||||||
|
|
||||||
-- Check a pattern clause, returning the component of the 'Case' expression it
|
-- Check a pattern clause, returning the component of the 'Case' expression it
|
||||||
-- represents, or Nothing if it's an impossible clause
|
-- represents, or Nothing if it's an impossible clause
|
||||||
@ -457,6 +470,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
|
|||||||
_ => pure ()
|
_ => pure ()
|
||||||
|
|
||||||
pure (Just (MkClause env' lhstm' rhstm))
|
pure (Just (MkClause env' lhstm' rhstm))
|
||||||
|
-- TODO: (to decide) With is complicated. Move this into its own module?
|
||||||
checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
|
checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
|
||||||
= do (vars' ** (sub', env', nest', lhspat, reqty)) <-
|
= do (vars' ** (sub', env', nest', lhspat, reqty)) <-
|
||||||
checkLHS mult hashit n opts nest env fc lhs_in
|
checkLHS mult hashit n opts nest env fc lhs_in
|
||||||
@ -470,7 +484,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
|
|||||||
clearHoleLHS
|
clearHoleLHS
|
||||||
|
|
||||||
logTerm 5 "With value" wval
|
logTerm 5 "With value" wval
|
||||||
logTerm 5 "Required type" reqty
|
logTerm 3 "Required type" reqty
|
||||||
wvalTy <- getTerm gwvalTy
|
wvalTy <- getTerm gwvalTy
|
||||||
defs <- get Ctxt
|
defs <- get Ctxt
|
||||||
wval <- normaliseHoles defs env' wval
|
wval <- normaliseHoles defs env' wval
|
||||||
@ -504,7 +518,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
|
|||||||
(weaken {n=wargn} notreqty))
|
(weaken {n=wargn} notreqty))
|
||||||
let bNotReq = Bind fc wargn (Pi RigW Explicit wvalTy) wtyScope
|
let bNotReq = Bind fc wargn (Pi RigW Explicit wvalTy) wtyScope
|
||||||
|
|
||||||
let Just (reqns, wtype) = bindReq fc env' withSub [] bNotReq
|
let Just (reqns, envns, wtype) = bindReq fc env' withSub [] bNotReq
|
||||||
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")
|
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")
|
||||||
|
|
||||||
-- list of argument names - 'Just' means we need to match the name
|
-- list of argument names - 'Just' means we need to match the name
|
||||||
@ -514,24 +528,30 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
|
|||||||
= map Just reqns ++
|
= map Just reqns ++
|
||||||
Nothing :: map Just notreqns
|
Nothing :: map Just notreqns
|
||||||
|
|
||||||
logTerm 5 "With function type" wtype
|
logTerm 3 "With function type" wtype
|
||||||
log 5 $ "Argument names " ++ show wargNames
|
log 5 $ "Argument names " ++ show wargNames
|
||||||
|
|
||||||
wname <- genWithName n
|
wname <- genWithName n
|
||||||
widx <- addDef wname (newDef fc wname mult vars wtype Private None)
|
widx <- addDef wname (newDef fc wname mult vars wtype Private None)
|
||||||
let rhs_in = apply (IVar fc wname)
|
let rhs_in = apply (IVar fc wname)
|
||||||
(map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
|
(map (IVar fc) envns ++
|
||||||
|
map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
|
||||||
|
|
||||||
|
log 3 $ "Applying to with argument " ++ show rhs_in
|
||||||
rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $
|
rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $
|
||||||
checkTermSub n wmode opts nest' env' env sub' rhs_in
|
checkTermSub n wmode opts nest' env' env sub' rhs_in
|
||||||
(gnf env' reqty)
|
(gnf env' reqty)
|
||||||
|
|
||||||
-- Generate new clauses by rewriting the matched arguments
|
-- Generate new clauses by rewriting the matched arguments
|
||||||
cs' <- traverse (mkClauseWith 1 wname wargNames lhs_in) cs
|
cs' <- traverse (mkClauseWith 1 wname wargNames lhs_in) cs
|
||||||
|
log 3 $ "With clauses: " ++ show cs'
|
||||||
|
|
||||||
-- Elaborate the new definition here
|
-- Elaborate the new definition here
|
||||||
|
nestname <- applyEnv env wname
|
||||||
|
let nest'' = record { names $= (nestname ::) } nest
|
||||||
|
|
||||||
let wdef = IDef fc wname cs'
|
let wdef = IDef fc wname cs'
|
||||||
processDecl [] nest env wdef
|
processDecl [] nest'' env wdef
|
||||||
|
|
||||||
pure (Just (MkClause env' lhspat rhs))
|
pure (Just (MkClause env' lhspat rhs))
|
||||||
where
|
where
|
||||||
@ -554,7 +574,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
|
|||||||
keepOldEnv (KeepCons p) (KeepCons p')
|
keepOldEnv (KeepCons p) (KeepCons p')
|
||||||
= let (_ ** rest) = keepOldEnv p p' in
|
= let (_ ** rest) = keepOldEnv p p' in
|
||||||
(_ ** KeepCons rest)
|
(_ ** KeepCons rest)
|
||||||
|
|
||||||
-- Rewrite the clauses in the block to use an updated LHS.
|
-- Rewrite the clauses in the block to use an updated LHS.
|
||||||
-- 'drop' is the number of additional with arguments we expect (i.e.
|
-- 'drop' is the number of additional with arguments we expect (i.e.
|
||||||
-- the things to drop from the end before matching LHSs)
|
-- the things to drop from the end before matching LHSs)
|
||||||
|
@ -170,6 +170,8 @@
|
|||||||
(micro (mod s 1000000)))
|
(micro (mod s 1000000)))
|
||||||
(sleep (make-time 'time-duration (* 1000 micro) sec))))
|
(sleep (make-time 'time-duration (* 1000 micro) sec))))
|
||||||
|
|
||||||
|
(define (blodwen-time) (time-second (current-time)))
|
||||||
|
|
||||||
(define (blodwen-args)
|
(define (blodwen-args)
|
||||||
(define (blodwen-build-args args)
|
(define (blodwen-build-args args)
|
||||||
(if (null? args)
|
(if (null? args)
|
||||||
|
Loading…
Reference in New Issue
Block a user