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

Check RHS and build PatAlt

Browse Source 
We need to be able to convert function arguments into Pats for this, and
so this also adds cases to Pat for matching on constants and types.
This commit is contained in:
Edwin Brady 2019-04-19 16:06:26 +01:00
parent c3f36ce484
commit 01572ec47a
7 changed files with 157 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Core/Context.idr
View File

@ -553,6 +553,12 @@ toFullNames tm
= pure (PAs fc idx x !(fullPat gam y))
fullPat gam (PCon fc x tag arity xs)
= pure (PCon fc x tag arity !(traverse (fullPat gam) xs))
fullPat gam (PTyCon fc x arity xs)
= pure (PTyCon fc x arity !(traverse (fullPat gam) xs))
fullPat gam (PConst fc c)
= pure (PConst fc c)
fullPat gam (PArrow fc x s t)
= pure (PArrow fc x !(fullPat gam s) !(fullPat gam t))
fullPat gam (PLoc fc idx x)
= pure (PLoc fc idx x)
fullPat gam (PUnmatchable fc x)

10
src/Core/Hash.idr
View File

@ -131,10 +131,16 @@ mutual
= h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` y
hashWithSalt h (PCon fc x tag arity xs)
= h `hashWithSalt` 1 `hashWithSalt` x `hashWithSalt` xs
hashWithSalt h (PTyCon fc x arity xs)
= h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` xs
hashWithSalt h (PConst fc c)
= h `hashWithSalt` 3 `hashWithSalt` (show c)
hashWithSalt h (PArrow fc x s t)
= h `hashWithSalt` 4 `hashWithSalt` s `hashWithSalt` t
hashWithSalt h (PLoc fc idx x)
= h `hashWithSalt` 2 `hashWithSalt` idx
= h `hashWithSalt` 5 `hashWithSalt` idx
hashWithSalt h (PUnmatchable fc x)
= h `hashWithSalt` 3 `hashWithSalt` x
= h `hashWithSalt` 6 `hashWithSalt` x
export
Hashable (PatAlt vars) where

52
src/Core/TT.idr
View File

@ -321,6 +321,10 @@ mutual
FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars
PCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
List (Pat vars) -> Pat vars
PTyCon : FC -> Name -> (arity : Nat) ->
List (Pat vars) -> Pat vars
PConst : FC -> (c : Constant) -> Pat vars
PArrow : FC -> (x : Name) -> Pat vars -> Pat (x :: vars) -> Pat vars
PLoc : {name : _} ->
FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars
PUnmatchable : FC -> Term vars -> Pat vars
@ -348,6 +352,22 @@ mutual
ConstCase : Constant -> CaseTree vars -> CaseAlt vars
DefaultCase : CaseTree vars -> CaseAlt vars
export
getLoc : Term vars -> FC
getLoc (Local fc x idx y) = fc
getLoc (Ref fc x name) = fc
getLoc (Meta fc x y xs) = fc
getLoc (Bind fc x b scope) = fc
getLoc (App fc fn p arg) = fc
getLoc (Case fc cs ty x alts) = fc
getLoc (As fc idx x y) = fc
getLoc (TDelayed fc x y) = fc
getLoc (TDelay fc x y) = fc
getLoc (TForce fc x) = fc
getLoc (PrimVal fc c) = fc
getLoc (Erased fc) = fc
getLoc (TType fc) = fc
export
Eq LazyReason where
(==) LInf LInf = True
@ -572,6 +592,11 @@ mutual
PAs fc _ prf' (thinPat n p)
thinPat n (PCon fc x tag arity args)
= PCon fc x tag arity (map (thinPat n) args)
thinPat n (PTyCon fc x arity args)
= PTyCon fc x arity (map (thinPat n) args)
thinPat n (PConst fc c) = PConst fc c
thinPat {outer} n (PArrow fc x s t)
= PArrow fc x (thinPat n s) (thinPat {outer = x :: outer} n t)
thinPat n (PLoc fc idx prf)
= let (_ ** prf') = insertVar {n} _ prf in
PLoc fc _ prf'
@ -584,6 +609,12 @@ mutual
PAs fc _ prf' (insertPatNames ns p)
insertPatNames ns (PCon fc x tag arity args)
= PCon fc x tag arity (map (insertPatNames ns) args)
insertPatNames ns (PTyCon fc x arity args)
= PTyCon fc x arity (map (insertPatNames ns) args)
insertPatNames ns (PConst fc c) = PConst fc c
insertPatNames {outer} ns (PArrow fc x s t)
= PArrow fc x (insertPatNames ns s)
(insertPatNames {outer = x :: outer} ns t)
insertPatNames ns (PLoc fc idx prf)
= let (_ ** prf') = insertVarNames {ns} _ prf in
PLoc fc _ prf'
@ -686,6 +717,11 @@ mutual
= PAs fc idx (snd (renameLocalRef prf p)) (renamePat prf pat)
renamePat prf (PCon fc x tag arity xs)
= PCon fc x tag arity (map (renamePat prf) xs)
renamePat prf (PTyCon fc x arity xs)
= PTyCon fc x arity (map (renamePat prf) xs)
renamePat prf (PConst fc c) = PConst fc c
renamePat prf (PArrow fc x s t)
= PArrow fc x (renamePat prf s) (renamePat (CompatExt prf) t)
renamePat prf (PLoc fc idx p)
= PLoc fc idx (snd (renameLocalRef prf p))
renamePat prf (PUnmatchable fc tm)
@ -790,6 +826,11 @@ mutual
Just (PAs fc _ x' !(shrinkPat pat prf))
shrinkPat (PCon fc x tag arity xs) prf
= Just (PCon fc x tag arity !(traverse (\x => shrinkPat x prf) xs))
shrinkPat (PTyCon fc tag arity xs) prf
= Just (PTyCon fc tag arity !(traverse (\x => shrinkPat x prf) xs))
shrinkPat (PConst fc c) prf = Just (PConst fc c)
shrinkPat (PArrow fc x s t) prf
= Just (PArrow fc x !(shrinkPat s prf) !(shrinkPat t (KeepCons prf)))
shrinkPat (PLoc fc idx x) prf
= case subElem x prf of
Nothing => Nothing
@ -906,6 +947,11 @@ mutual
PAs fc _ p' (mkLocalPat bs pat)
mkLocalPat bs (PCon fc x tag arity args)
= PCon fc x tag arity (map (mkLocalPat bs) args)
mkLocalPat bs (PTyCon fc x arity args)
= PTyCon fc x arity (map (mkLocalPat bs) args)
mkLocalPat bs (PConst fc c) = PConst fc c
mkLocalPat {later} bs (PArrow fc x s t)
= PArrow fc x (mkLocalPat bs s) (mkLocalPat {later = x :: later} bs t)
mkLocalPat bs (PLoc fc idx p)
= let (_ ** p') = addVars bs p in
PLoc fc _ p'
@ -1006,6 +1052,9 @@ getMetas tm = getMap empty tm
getPatMap : NameMap () -> Pat vars -> NameMap ()
getPatMap ns (PAs fc idx x y) = getPatMap ns y
getPatMap ns (PCon fc x tag arity xs) = getAll getPatMap ns xs
getPatMap ns (PTyCon fc x arity xs) = getAll getPatMap ns xs
getPatMap ns (PConst fc c) = ns
getPatMap ns (PArrow fc x s t) = getPatMap (getPatMap ns s) t
getPatMap ns (PLoc fc idx x) = ns
getPatMap ns (PUnmatchable fc x) = getMap ns x
@ -1062,6 +1111,9 @@ getRefs tm = getMap empty tm
getPatMap : NameMap () -> Pat vars -> NameMap ()
getPatMap ns (PAs fc idx x y) = getPatMap ns y
getPatMap ns (PCon fc x tag arity xs) = getAll getPatMap ns xs
getPatMap ns (PTyCon fc x arity xs) = getAll getPatMap ns xs
getPatMap ns (PConst fc c) = ns
getPatMap ns (PArrow fc x s t) = getPatMap (getPatMap ns s) t
getPatMap ns (PLoc fc idx x) = ns
getPatMap ns (PUnmatchable fc x) = getMap ns x

25
src/Core/TTC.idr
View File

@ -276,11 +276,17 @@ mutual
toBuf b (PAs {name} fc idx x y)
= do tag 0; toBuf b fc; toBuf b name; toBuf b idx; toBuf b y
toBuf b (PCon fc x t arity xs)
= do tag 1; toBuf b fc; toBuf b t; toBuf b arity; toBuf b xs
= do tag 1; toBuf b fc; toBuf b x; toBuf b t; toBuf b arity; toBuf b xs
toBuf b (PTyCon fc x arity xs)
= do tag 2; toBuf b fc; toBuf b x; toBuf b arity; toBuf b xs
toBuf b (PConst fc c)
= do tag 3; toBuf b fc; toBuf b c
toBuf b (PArrow fc x s t)
= do tag 4; toBuf b fc; toBuf b x; toBuf b s; toBuf b t
toBuf b (PLoc {name} fc idx x)
= do tag 2; toBuf b fc; toBuf b name; toBuf b idx
= do tag 5; toBuf b fc; toBuf b name; toBuf b idx
toBuf b (PUnmatchable fc x)
= do tag 3; toBuf b fc; toBuf b x
= do tag 6; toBuf b fc; toBuf b x
fromBuf r b
= case !getTag of
@ -291,10 +297,19 @@ mutual
t <- fromBuf r b; arity <- fromBuf r b
xs <- fromBuf r b
pure (PCon fc x t arity xs)
2 => do fc <- fromBuf r b; name <- fromBuf r b
2 => do fc <- fromBuf r b; x <- fromBuf r b
arity <- fromBuf r b
xs <- fromBuf r b
pure (PTyCon fc x arity xs)
3 => do fc <- fromBuf r b; c <- fromBuf r b
pure (PConst fc c)
4 => do fc <- fromBuf r b; x <- fromBuf r b
s <- fromBuf r b; t <- fromBuf r b
pure (PArrow fc x s t)
5 => do fc <- fromBuf r b; name <- fromBuf r b
idx <- fromBuf r b
pure (PLoc {name} fc idx (mkPrf idx))
3 => do fc <- fromBuf r b; x <- fromBuf r b
6 => do fc <- fromBuf r b; x <- fromBuf r b
pure (PUnmatchable fc x)
_ => corrupt "Pat"

10
src/TTImp/Elab.idr
View File

@ -25,3 +25,13 @@ elabTerm defining mode env tm ty
= do e <- newRef EST (initEState defining env)
let rigc = getRigNeeded mode
check {e} rigc (initElabInfo mode) env tm ty
export
checkTerm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Name -> ElabMode -> Env Term vars -> RawImp -> Glued vars ->
Core (Term vars)
checkTerm defining mode env tm ty
= do (tm_elab, _) <- elabTerm defining mode env tm (Just ty)
pure tm_elab

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

@ -75,6 +75,12 @@ mutual
PAs fc _ x' (embedPat sub y)
embedPat sub (PCon fc x tag arity xs)
= PCon fc x tag arity (map (embedPat sub) xs)
embedPat sub (PTyCon fc x arity xs)
= PTyCon fc x arity (map (embedPat sub) xs)
embedPat sub (PConst fc c)
= PConst fc c
embedPat sub (PArrow fc x s t)
= PArrow fc x (embedPat sub s) (embedPat (KeepCons sub) t)
embedPat sub (PLoc fc idx x)
= let (_ ** x') = varEmbedSub sub x in
PLoc fc _ x'
@ -282,6 +288,11 @@ mutual
= let (_ ** p') = swapIsVar _ p in PAs fc _ p' (swapPat pat)
swapPat (PCon fc x tag arity xs)
= PCon fc x tag arity (map swapPat xs)
swapPat (PTyCon fc x arity xs)
= PTyCon fc x arity (map swapPat xs)
swapPat (PConst fc c) = PConst fc c
swapPat {vs} (PArrow fc x s t)
= PArrow fc x (swapPat s) (swapPat {vs = x :: vs} t)
swapPat (PLoc fc idx p)
= let (_ ** p') = swapIsVar _ p in PLoc fc _ p'
swapPat (PUnmatchable fc x) = PUnmatchable fc (swapVars x)
@ -527,9 +538,10 @@ checkBindHere rig elabinfo env fc bindmode tm exp
est <- get EST
put EST (updateEnv oldenv oldsub oldbif
(record { boundNames = [] } est))
ty <- getTerm tmt
(bv, bt) <- bindImplicits fc bindmode
defs env argImps
!(normaliseHoles defs env tmv)
(TType fc)
!(normaliseHoles defs env ty)
traverse implicitBind (map fst argImps)
checkExp rig elabinfo env fc bv (gnf defs env bt) exp

51
src/TTImp/ProcessDef.idr
View File

@ -10,6 +10,42 @@ import TTImp.Elab
import TTImp.Elab.Check
import TTImp.TTImp
mkPat' : List (Pat vars) -> Term vars -> Term vars -> Pat vars
mkPat' [] orig (Local fc c idx p) = PLoc fc idx p
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)
= 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' args orig (As fc idx p ptm)
= let pat = mkPat' args orig ptm in
PAs fc idx p pat
mkPat' [] orig (PrimVal fc c) = PConst fc c
mkPat' args orig tm = PUnmatchable (getLoc orig) orig
mkPat : Term vars -> Pat vars
mkPat tm = mkPat' [] tm tm
-- Given a type checked LHS and its type, return the environment in which we
-- should check the RHS, the LHS and its type in that environment,
-- and a function which turns a checked RHS into a
-- pattern clause
extendEnv : Env Term vars ->
Term vars -> Term vars ->
(PatAlt vars -> a) ->
Core (vars' ** (Env Term vars',
Term vars', Term vars',
List (Pat vars') -> Term vars' -> a))
extendEnv env (Bind _ n (PVar c tmty) sc) (Bind _ n' (PVTy _ _) tysc) p with (nameEq n n')
extendEnv env (Bind _ n (PVar c tmty) sc) (Bind _ n' (PVTy _ _) tysc) p | Nothing
= throw (InternalError "Can't happen: names don't match in pattern type")
extendEnv env (Bind _ n (PVar c tmty) sc) (Bind _ n (PVTy _ _) tysc) p | (Just Refl)
= extendEnv (PVar c tmty :: env) sc tysc (\alt => p (CBind c n tmty alt))
extendEnv env tm ty p
= pure (_ ** (env, tm, ty, \pats, rhs => p (CPats pats rhs)))
-- Check a pattern clause, returning the component of the 'Case' expression it
-- represents, or Nothing if it's an impossible clause
export
@ -22,11 +58,20 @@ checkClause mult hashit n env (ImpossibleClause fc lhs)
= throw (InternalError "impossible not implemented yet")
checkClause mult hashit n env (PatClause fc lhs_in rhs)
= do lhs <- lhsInCurrentNS lhs_in
(lhstm, lhsty) <- elabTerm n (InLHS mult) env
(lhstm, lhstyg) <- elabTerm n (InLHS mult) env
(IBindHere fc PATTERN lhs) Nothing
lhsty <- getTerm lhstyg
logTermNF 0 "LHS term" env lhstm
logGlue 0 "LHS type" env lhsty
?checkPat
logTermNF 0 "LHS type" env lhsty
(vars' ** (env', lhstm', lhsty', mkAlt)) <-
extendEnv env lhstm lhsty id
defs <- get Ctxt
rhstm <- checkTerm n InExpr env' rhs (gnf defs env' lhsty')
logTermNF 0 "RHS term" env' rhstm
pure (Just (mkAlt (map (mkPat . snd) (getArgs lhstm')) rhstm))
export
processDef : {auto c : Ref Ctxt Defs} ->