Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update for GHC8 and (partial) fix of assertion patterns checking #4

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Update for GHC8 and (partial) fix of assertion patterns checking #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5eaa216
SimpleFP-v2: make it compile with GHC8 and lts-8.13
yanok May 15, 2017
d633820
SimpleFP-v2: add stack.yaml
yanok May 15, 2017
1af13ab
dependent: add example that show we can (wrongly) prove injectivity
yanok May 15, 2017
c76d50e
Dependent: add example of (wrongly) proving equality for any pair of …
yanok May 30, 2017
4478f71
typecheck: fix assertion patterns checking
yanok Jun 2, 2017
290c986
unification: change the way unification works
yanok Jun 2, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 9 additions & 8 deletions src/Continuations/Core/Term.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,14 +142,15 @@ instance Bizippable PatternFF where


instance Bitraversable PatternFF where
bisequenceA (ConPat c ps) =
ConPat c <$> sequenceA [ (,) plic <$> p
| (plic,p) <- ps
]
bisequenceA (AssertionPat m) =
AssertionPat <$> m
bisequenceA MakeMeta =
pure MakeMeta
bitraverse f g = biseq . bimap f g where
biseq (ConPat c ps) =
ConPat c <$> sequenceA [ (,) plic <$> p
| (plic,p) <- ps
]
biseq (AssertionPat m) =
AssertionPat <$> m
biseq MakeMeta =
pure MakeMeta


-- | 'PatternF' is the type of pattern shaped containers for terms. The
Expand Down
84 changes: 53 additions & 31 deletions src/Continuations/Unification/TypeChecking.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -344,7 +344,7 @@ inferify (Var (Free x)) =
return (ElaboratedTerm (Var (Free x)), t)
inferify (Var (Bound _ _)) =
error "Bound type variables should not be the subject of type checking."
inferify (Var (Meta x)) =
inferify (Var (Meta _ x)) =
throwError $ "The metavariable " ++ show x
++ " appears in checkable code, when it should not."
inferify (In (Defined x)) =
Expand Down Expand Up @@ -550,8 +550,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
++ pretty (appH Impl f m)
inferifyApplication f (In (Fun Impl _ sc)) Expl m =
do meta <- nextElab nextMeta
let f' = appH Impl f (Var (Meta meta))
t' = instantiate sc [Var (Meta meta)]
let f' = appH Impl f (Var (Meta Exist meta))
t' = instantiate sc [Var (Meta Exist meta)]
inferifyApplication f' t' Expl m
inferifyApplication f _ _ _ =
throwError $ "Cannot apply non-function: " ++ pretty f
Expand Down Expand Up @@ -608,7 +608,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
go (acc ++ [(Impl,m')]) ascs bsc ms
go acc ((Impl,_):ascs) bsc ms =
do meta <- nextElab nextMeta
go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
go _ _ _ _ =
throwError "Cannot match signature."

Expand Down Expand Up @@ -886,7 +886,7 @@ checkifyConArgs ascs0 bsc ms0 t =
return acc
accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
xs = [ x' | (_,_,x',_) <- acc ]
newSuspension = (Expl, Just m, x, instantiate asc xs)
accArgsToCheck
Expand All @@ -895,7 +895,7 @@ checkifyConArgs ascs0 bsc ms0 t =
ms
accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
xs = [ x' | (_,_,x',_) <- acc ]
newSuspension = (Impl, Just m, x, instantiate asc xs)
accArgsToCheck
Expand All @@ -904,7 +904,7 @@ checkifyConArgs ascs0 bsc ms0 t =
ms
accArgsToCheck acc ((Impl,asc):ascs) ms =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
xs = [ x' | (_,_,x',_) <- acc ]
newSuspension = (Impl, Nothing, x, instantiate asc xs)
accArgsToCheck
Expand All @@ -917,12 +917,12 @@ checkifyConArgs ascs0 bsc ms0 t =
swapMetas :: [(Plicity,Term)]
-> TypeChecker ([(Term,Term)], [(Plicity,Term)])
swapMetas [] = return ([],[])
swapMetas ((plic, Var (Meta meta)):ms) =
swapMetas ((plic, Var (Meta Exist meta)):ms) =
do (eqs,ms') <- swapMetas ms
return (eqs, (plic,Var (Meta meta)):ms')
return (eqs, (plic,Var (Meta Exist meta)):ms')
swapMetas ((plic,m):ms) =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
(eqs,ms') <- swapMetas ms
return ((x,m):eqs, (plic,x):ms')

Expand Down Expand Up @@ -978,20 +978,21 @@ checkifyCaseMotive (CaseMotive tele) =

checkifyPattern :: Pattern
-> NormalTerm
-> TypeChecker (Pattern,ElaboratedTerm)
-> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
checkifyPattern (Var (Bound _ _)) _ =
error "A bound variable should not be the subject of pattern type checking."
checkifyPattern (Var (Free x)) t =
do QLJ t' _ <- typeInContext x
unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal
return ( Var (Free x)
, ElaboratedTerm (Var (Free x))
, []
)
checkifyPattern (Var (Meta _)) _ =
checkifyPattern (Var (Meta _ _)) _ =
error "Metavariables should not be the subject of pattern type checking."
checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
(ps',elms') <-
(ps',elms',cs) <-
checkifyPatterns
(zip plics ascs)
bsc
Expand All @@ -1000,17 +1001,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
return ( conPatH ec ps'
, ElaboratedTerm (conH ec ms')
, cs
)
checkifyPattern (In (AssertionPat m)) t =
do ElaboratedTerm m' <- checkify m t
mv <- nextElab nextMeta
return ( In (AssertionPat m')
, ElaboratedTerm m'
, ElaboratedTerm (Var $ Meta Constraint mv)
, [(Var $ Meta Constraint mv, m')]
)
checkifyPattern (In MakeMeta) _ =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
return ( In (AssertionPat x)
, ElaboratedTerm x
, []
)


Expand Down Expand Up @@ -1049,6 +1054,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
-> Term
-> TypeChecker ( [(Plicity,Pattern)]
, [(Plicity,ElaboratedTerm)]
, [(Term,Term)]
)
checkifyPatterns ascs0 bsc ps0 t =
do argsToCheck <- accArgsToCheck [] ascs0 ps0
Expand All @@ -1062,33 +1068,36 @@ checkifyPatterns ascs0 bsc ps0 t =
return (eqs,ret')
ret' -> return ([],ret')
unifyHelper (NormalTerm ret') (NormalTerm t)
psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
(ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
case p0 of
Nothing ->
do subMToElabInto <- substitute mToElabInto
em' <- evaluate subMToElabInto
return ( (plic, In (AssertionPat (normTerm em')))
, (plic, ElaboratedTerm (normTerm em'))
, []
)
Just p ->
do subMToElabInto <- substitute mToElabInto
eMToElabInto <- evaluate subMToElabInto
suba <- substitute a
ea <- evaluate suba
(p',ElaboratedTerm m') <- checkifyPattern p ea
(p',ElaboratedTerm m',cs) <- checkifyPattern p ea
subm' <- substitute m'
em' <- evaluate subm'
unifyHelper eMToElabInto em'
return ( (plic, p')
, (plic, ElaboratedTerm (normTerm em'))
, cs
)
)
forM_ eqs $ \(l,r) ->
do subl <- substitute l
el <- evaluate subl
subr <- substitute r
er <- evaluate subr
unifyHelper el er
return $ unzip psms'
return (ps',ms',concat cs)
where
accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
-> [(Plicity,Scope TermF)]
Expand All @@ -1098,7 +1107,7 @@ checkifyPatterns ascs0 bsc ps0 t =
return acc
accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
xs = [ x' | (_,_,x',_) <- acc ]
newSuspension = (Expl, Just p, x, instantiate asc xs)
accArgsToCheck
Expand All @@ -1107,7 +1116,7 @@ checkifyPatterns ascs0 bsc ps0 t =
ps
accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
xs = [ x' | (_,_,x',_) <- acc ]
newSuspension = (Impl, Just p, x, instantiate asc xs)
accArgsToCheck
Expand All @@ -1116,7 +1125,7 @@ checkifyPatterns ascs0 bsc ps0 t =
ps
accArgsToCheck acc ((Impl,asc):ascs) ps =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
xs = [ x' | (_,_,x',_) <- acc ]
newSuspension = (Impl, Nothing, x, instantiate asc xs)
accArgsToCheck
Expand All @@ -1129,12 +1138,12 @@ checkifyPatterns ascs0 bsc ps0 t =
swapMetas :: [(Plicity,Term)]
-> TypeChecker ([(Term,Term)], [(Plicity,Term)])
swapMetas [] = return ([],[])
swapMetas ((plic, Var (Meta meta)):ms) =
swapMetas ((plic, Var (Meta Exist meta)):ms) =
do (eqs,ms') <- swapMetas ms
return (eqs, (plic,Var (Meta meta)):ms')
return (eqs, (plic,Var (Meta Exist meta)):ms')
swapMetas ((plic,m):ms) =
do meta <- nextElab nextMeta
let x = Var (Meta meta)
let x = Var (Meta Exist meta)
(eqs,ms') <- swapMetas ms
return ((x,m):eqs, (plic,x):ms')

Expand All @@ -1160,21 +1169,34 @@ checkifyPatternsCaseMotive :: [Pattern]
-> CaseMotive
-> TypeChecker ([Pattern], ElaboratedTerm)
checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
do (ps',ms') <- go [] ps0 ascs
do (ps',ms',cs) <- go [] ps0 ascs
forM_ cs (\(l,r) -> do
subl <- substitute l
el <- evaluate subl
subr <- substitute r
er <- evaluate subr
s <- getElab substitution
unifyHelper el er
s' <- getElab substitution
when (length s /= length s') $
throwError $ "Solving the constraint "
++ pretty (normTerm el) ++ " == "
++ pretty (normTerm er) ++ " produced new metavar resolution"
)
return (ps', ElaboratedTerm (instantiate bsc ms'))
where
go :: [Term]
-> [Pattern]
-> [Scope TermF]
-> TypeChecker ([Pattern],[Term])
-> TypeChecker ([Pattern],[Term],[(Term,Term)])
go _ [] [] =
return ([],[])
return ([],[],[])
go acc (p:ps) (sc:scs) =
do subt <- substitute (instantiate sc acc)
et <- evaluate subt
(p',ElaboratedTerm m') <- checkifyPattern p et
(ps',ms') <- go (acc ++ [m']) ps scs
return (p':ps', m':ms')
(p',ElaboratedTerm m',cs) <- checkifyPattern p et
(ps',ms',cs') <- go (acc ++ [m']) ps scs
return (p':ps', m':ms', cs ++ cs')
go _ _ _ =
error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
++ " should always have equal number of args for its patterns and"
Expand Down Expand Up @@ -1208,7 +1230,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
l <- getElab quoteLevel
ctx' <- forM ns $ \n ->
do m <- nextElab nextMeta
return (n, QLJ (Var (Meta m)) l)
return (n, QLJ (Var (Meta Exist m)) l)
extendElab context ctx' $
do (ps',ElaboratedTerm ret) <-
checkifyPatternsCaseMotive
Expand Down
Loading