mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-28 05:32:03 +03:00
Build patterns from closed terms
We'll use fresh names for the variables in the environment, then recalculate the local variables as we build the case tree (we don't know how many we'll need in advance, especially given 'as' patterns) Also implement 'subst' for this (it may turn out to have other uses too)
This commit is contained in:
Edwin Brady
parent
82ac86bde0
commit
dc3c0da2a0
@ -1,8 +1,35 @@
|
||||
module Core.CaseBuilder
|
||||
|
||||
import Core.CaseTree
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Normalise
|
||||
import Core.TT
|
||||
import Core.Value
|
||||
|
||||
%default covering
|
||||
|
||||
public export
|
||||
data Phase = CompileTime | RunTime
|
||||
|
||||
data ArgType : List Name -> Type where
|
||||
Known : RigCount -> (ty : Term vars) -> ArgType vars -- arg has type 'ty'
|
||||
Stuck : (fty : Term vars) -> ArgType vars
|
||||
-- ^ arg will have argument type of 'fty' when we know enough to
|
||||
-- calculate it
|
||||
Unknown : ArgType vars
|
||||
-- arg's type is not yet known due to a previously stuck argument
|
||||
|
||||
Show (ArgType ns) where
|
||||
show (Known c t) = "Known " ++ show c ++ " " ++ show t
|
||||
show (Stuck t) = "Stuck " ++ show t
|
||||
show Unknown = "Unknown"
|
||||
|
||||
record PatInfo (pvar : Name) (vars : List Name) where
|
||||
constructor MkInfo
|
||||
pat : Pat
|
||||
loc : IsVar name idx vars
|
||||
argType : ArgType vars -- Type of the argument being inspected (i.e.
|
||||
-- *not* refined by this particular pattern)
|
||||
|
||||
|
||||
|
||||
@ -21,18 +21,15 @@ mutual
|
||||
DefaultCase : CaseTree vars -> CaseAlt vars
|
||||
|
||||
public export
|
||||
data Pat : List Name -> Type where
|
||||
PAs : {name : _} ->
|
||||
FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars
|
||||
data Pat : Type where
|
||||
PAs : FC -> Name -> Pat -> Pat
|
||||
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
|
||||
List Pat -> Pat
|
||||
PTyCon : FC -> Name -> (arity : Nat) -> List Pat -> Pat
|
||||
PConst : FC -> (c : Constant) -> Pat
|
||||
PArrow : FC -> (x : Name) -> Pat -> Pat -> Pat
|
||||
PLoc : FC -> Name -> Pat
|
||||
PUnmatchable : FC -> Term [] -> Pat
|
||||
|
||||
mutual
|
||||
export
|
||||
@ -54,23 +51,23 @@ mutual
|
||||
show (DefaultCase sc)
|
||||
= "_ => " ++ show sc
|
||||
|
||||
mkPat' : List (Pat vars) -> Term vars -> Term vars -> Pat vars
|
||||
mkPat' [] orig (Local fc c idx p) = PLoc fc idx p
|
||||
mkPat' : List Pat -> Term [] -> Term [] -> Pat
|
||||
mkPat' [] orig (Ref fc Bound n) = PLoc fc n
|
||||
mkPat' args orig (Ref fc (DataCon t a) n) = PCon fc n t a args
|
||||
mkPat' args orig (Ref fc (TyCon t a) n) = PTyCon fc n a args
|
||||
mkPat' [] orig (Bind fc x (Pi _ _ s) t)
|
||||
= PArrow fc x (mkPat' [] s s) (mkPat' [] t t)
|
||||
= let t' = subst (Erased fc) t in
|
||||
PArrow fc x (mkPat' [] s s) (mkPat' [] t' t')
|
||||
mkPat' args orig (App fc fn p arg)
|
||||
= let parg = mkPat' [] arg arg in
|
||||
mkPat' (parg :: args) orig fn
|
||||
mkPat' args orig (As fc idx p ptm)
|
||||
= let pat = mkPat' args orig ptm in
|
||||
PAs fc idx p pat
|
||||
mkPat' [] orig (As fc (Ref _ Bound n) ptm)
|
||||
= PAs fc n (mkPat' [] ptm ptm)
|
||||
mkPat' [] orig (PrimVal fc c) = PConst fc c
|
||||
mkPat' args orig tm = PUnmatchable (getLoc orig) orig
|
||||
|
||||
export
|
||||
mkPat : Term vars -> Pat vars
|
||||
mkPat : Term [] -> Pat
|
||||
mkPat tm = mkPat' [] tm tm
|
||||
|
||||
mutual
|
||||
|
||||
@ -61,7 +61,7 @@ parameters (defs : Defs, opts : EvalOpts)
|
||||
(\arg => eval env (arg :: locs) scope stk)
|
||||
eval env locs (App fc fn p arg) stk
|
||||
= eval env locs fn ((p, MkClosure opts locs env arg) :: stk)
|
||||
eval env locs (As fc idx p tm) stk = eval env locs tm stk
|
||||
eval env locs (As fc _ tm) stk = eval env locs tm stk
|
||||
eval env locs (TDelayed fc r ty) stk
|
||||
= pure (NDelayed fc r (MkClosure opts locs env ty))
|
||||
eval env locs (TDelay fc r tm) stk
|
||||
|
||||
@ -297,9 +297,8 @@ data Term : List Name -> Type where
|
||||
App : FC -> (fn : Term vars) -> (p : AppInfo) -> (arg : Term vars) -> Term vars
|
||||
-- as patterns; since we check LHS patterns as terms before turning
|
||||
-- them into patterns, this helps us get it right. When normalising,
|
||||
-- we just reduce the inner term and ignore the name
|
||||
As : {name : _} ->
|
||||
FC -> (idx : Nat) -> IsVar name idx vars -> Term vars -> Term vars
|
||||
-- we just reduce the inner term and ignore the 'as' part
|
||||
As : FC -> (as : Term vars) -> (pat : Term vars) -> Term vars
|
||||
-- Typed laziness annotations
|
||||
TDelayed : FC -> LazyReason -> Term vars -> Term vars
|
||||
TDelay : FC -> LazyReason -> Term vars -> Term vars
|
||||
@ -315,7 +314,7 @@ 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 (As fc idx x y) = fc
|
||||
getLoc (As fc x y) = fc
|
||||
getLoc (TDelayed fc x y) = fc
|
||||
getLoc (TDelay fc x y) = fc
|
||||
getLoc (TForce fc x) = fc
|
||||
@ -454,9 +453,7 @@ thin {outer} {inner} n (Bind fc x b scope)
|
||||
= let sc' = thin {outer = x :: outer} {inner} n scope in
|
||||
Bind fc x (assert_total (map (thin n) b)) sc'
|
||||
thin n (App fc fn p arg) = App fc (thin n fn) p (thin n arg)
|
||||
thin n (As fc idx prf tm)
|
||||
= let (_ ** prf') = insertVar {n} _ prf in
|
||||
As fc _ prf' (thin n tm)
|
||||
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 tm) = TDelay fc r (thin n tm)
|
||||
thin n (TForce fc tm) = TForce fc (thin n tm)
|
||||
@ -479,9 +476,8 @@ insertNames {outer} {inner} ns (Bind fc x b scope)
|
||||
(insertNames {outer = x :: outer} {inner} ns scope)
|
||||
insertNames ns (App fc fn p arg)
|
||||
= App fc (insertNames ns fn) p (insertNames ns arg)
|
||||
insertNames ns (As fc idx prf tm)
|
||||
= let (_ ** prf') = insertVarNames {ns} idx prf in
|
||||
As fc _ prf' (insertNames ns tm)
|
||||
insertNames ns (As fc as tm)
|
||||
= As fc (insertNames ns as) (insertNames ns tm)
|
||||
insertNames ns (TDelayed fc r ty) = TDelayed fc r (insertNames ns ty)
|
||||
insertNames ns (TDelay fc r tm) = TDelay fc r (insertNames ns tm)
|
||||
insertNames ns (TForce fc tm) = TForce fc (insertNames ns tm)
|
||||
@ -547,8 +543,8 @@ renameVars prf (Bind fc x b scope)
|
||||
= Bind fc x (map (renameVars prf) b) (renameVars (CompatExt prf) scope)
|
||||
renameVars prf (App fc fn p arg)
|
||||
= App fc (renameVars prf fn) p (renameVars prf arg)
|
||||
renameVars prf (As fc idx vprf tm)
|
||||
= As fc idx (snd (renameLocalRef prf vprf)) (renameVars prf tm)
|
||||
renameVars prf (As fc as tm)
|
||||
= As fc (renameVars prf as) (renameVars prf tm)
|
||||
renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
|
||||
renameVars prf (TDelay fc r tm) = TDelay fc r (renameVars prf tm)
|
||||
renameVars prf (TForce fc x) = TForce fc (renameVars prf x)
|
||||
@ -620,10 +616,8 @@ mutual
|
||||
= Just (Bind fc x !(shrinkBinder b prf) !(shrinkTerm scope (KeepCons prf)))
|
||||
shrinkTerm (App fc fn p arg) prf
|
||||
= Just (App fc !(shrinkTerm fn prf) p !(shrinkTerm arg prf))
|
||||
shrinkTerm (As fc idx loc tm) prf
|
||||
= case subElem loc prf of
|
||||
Nothing => Nothing
|
||||
Just (_ ** loc') => Just (As fc _ loc' !(shrinkTerm tm prf))
|
||||
shrinkTerm (As fc as tm) prf
|
||||
= Just (As fc !(shrinkTerm as prf) !(shrinkTerm tm prf))
|
||||
shrinkTerm (TDelayed fc x y) prf
|
||||
= Just (TDelayed fc x !(shrinkTerm y prf))
|
||||
shrinkTerm (TDelay fc x y) prf
|
||||
@ -695,8 +689,8 @@ mkLocals {later} bs (Bind fc x b scope)
|
||||
(mkLocals {later = x :: later} bs scope)
|
||||
mkLocals bs (App fc fn p arg)
|
||||
= App fc (mkLocals bs fn) p (mkLocals bs arg)
|
||||
mkLocals bs (As fc idx p tm)
|
||||
= let (_ ** p') = addVars bs p in As fc _ p' (mkLocals bs tm)
|
||||
mkLocals bs (As fc as tm)
|
||||
= As fc (mkLocals bs as) (mkLocals bs tm)
|
||||
mkLocals bs (TDelayed fc x y)
|
||||
= TDelayed fc x (mkLocals bs y)
|
||||
mkLocals bs (TDelay fc x y)
|
||||
@ -711,6 +705,56 @@ export
|
||||
refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
|
||||
refsToLocals bs y = mkLocals {later = []} bs y
|
||||
|
||||
-- Substitute some explicit terms for names in a term, and remove those
|
||||
-- names from the scope
|
||||
namespace SubstEnv
|
||||
data SubstEnv : List Name -> List Name -> Type where
|
||||
Nil : SubstEnv [] vars
|
||||
(::) : Term vars ->
|
||||
SubstEnv ds vars -> SubstEnv (d :: ds) vars
|
||||
|
||||
findDrop : {drop, idx : _} ->
|
||||
FC -> Maybe RigCount -> IsVar name idx (drop ++ vars) ->
|
||||
SubstEnv drop vars -> Term vars
|
||||
findDrop {drop = []} fc r var env = Local fc r _ var
|
||||
findDrop {drop = x :: xs} fc r First (tm :: env) = tm
|
||||
findDrop {drop = x :: xs} fc r (Later p) (tm :: env)
|
||||
= findDrop fc r p env
|
||||
|
||||
find : {outer, idx : _} ->
|
||||
FC -> Maybe RigCount -> IsVar name idx (outer ++ (drop ++ vars)) ->
|
||||
SubstEnv drop vars ->
|
||||
Term (outer ++ vars)
|
||||
find {outer = []} fc r var env = findDrop fc r var env
|
||||
find {outer = x :: xs} fc r First env = Local fc r _ First
|
||||
find {outer = x :: xs} fc r (Later p) env = weaken (find fc r p env)
|
||||
|
||||
substEnv : {outer : _} ->
|
||||
SubstEnv drop vars -> Term (outer ++ (drop ++ vars)) ->
|
||||
Term (outer ++ vars)
|
||||
substEnv env (Local fc r _ prf)
|
||||
= find fc r prf env
|
||||
substEnv env (Ref fc x name) = Ref fc x name
|
||||
substEnv env (Meta fc n i xs)
|
||||
= Meta fc n i (map (substEnv env) xs)
|
||||
substEnv {outer} env (Bind fc x b scope)
|
||||
= Bind fc x (map (substEnv env) b)
|
||||
(substEnv {outer = x :: outer} env scope)
|
||||
substEnv env (App fc fn p arg)
|
||||
= App fc (substEnv env fn) p (substEnv env arg)
|
||||
substEnv env (As fc as pat)
|
||||
= As fc (substEnv env as) (substEnv env pat)
|
||||
substEnv env (TDelayed fc x y) = TDelayed fc x (substEnv env y)
|
||||
substEnv env (TDelay fc x y) = TDelay fc x (substEnv env y)
|
||||
substEnv env (TForce fc x) = TForce fc (substEnv env x)
|
||||
substEnv env (PrimVal fc c) = PrimVal fc c
|
||||
substEnv env (Erased fc) = Erased fc
|
||||
substEnv env (TType fc) = TType fc
|
||||
|
||||
export
|
||||
subst : Term vars -> Term (x :: vars) -> Term vars
|
||||
subst val tm = substEnv {outer = []} {drop = [_]} [val] tm
|
||||
|
||||
-- Get the metavariable names in a term
|
||||
export
|
||||
getMetas : Term vars -> NameMap ()
|
||||
@ -726,7 +770,7 @@ getMetas tm = getMap empty tm
|
||||
= getMap (getMap ns (binderType b)) scope
|
||||
getMap ns (App fc fn p arg)
|
||||
= getMap (getMap ns fn) arg
|
||||
getMap ns (As fc idx x y) = getMap ns y
|
||||
getMap ns (As fc as tm) = getMap ns tm
|
||||
getMap ns (TDelayed fc x y) = getMap ns y
|
||||
getMap ns (TDelay fc x y) = getMap ns y
|
||||
getMap ns (TForce fc x) = getMap ns x
|
||||
@ -750,7 +794,7 @@ getRefs tm = getMap empty tm
|
||||
= getMap (getMap ns (binderType b)) scope
|
||||
getMap ns (App fc fn p arg)
|
||||
= getMap (getMap ns fn) arg
|
||||
getMap ns (As fc idx x y) = getMap ns y
|
||||
getMap ns (As fc as tm) = getMap ns tm
|
||||
getMap ns (TDelayed fc x y) = getMap ns y
|
||||
getMap ns (TDelay fc x y) = getMap ns y
|
||||
getMap ns (TForce fc x) = getMap ns x
|
||||
|
||||
@ -210,10 +210,9 @@ TTC (Term vars) where
|
||||
toBuf b (App fc fn p arg)
|
||||
= do tag 4;
|
||||
toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg
|
||||
toBuf b (As {name} fc idx p tm)
|
||||
toBuf b (As fc as tm)
|
||||
= do tag 5;
|
||||
toBuf b fc; toBuf b name;
|
||||
toBuf b idx; toBuf b tm
|
||||
toBuf b fc; toBuf b as; toBuf b tm
|
||||
toBuf b (TDelayed fc r tm)
|
||||
= do tag 6;
|
||||
toBuf b fc; toBuf b r; toBuf b tm
|
||||
@ -249,9 +248,9 @@ TTC (Term vars) where
|
||||
4 => do fc <- fromBuf r b; fn <- fromBuf r b
|
||||
p <- fromBuf r b; arg <- fromBuf r b
|
||||
pure (App fc fn p arg)
|
||||
5 => do fc <- fromBuf r b; name <- fromBuf r b
|
||||
idx <- fromBuf r b; tm <- fromBuf r b
|
||||
pure (As {name} fc idx (mkPrf idx) tm)
|
||||
5 => do fc <- fromBuf r b
|
||||
as <- fromBuf r b; tm <- fromBuf r b
|
||||
pure (As fc as tm)
|
||||
6 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
|
||||
pure (TDelayed fc lr tm)
|
||||
7 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
|
||||
@ -265,9 +264,9 @@ TTC (Term vars) where
|
||||
_ => corrupt "Term"
|
||||
|
||||
export
|
||||
TTC (Pat vars) where
|
||||
toBuf b (PAs {name} fc idx x y)
|
||||
= do tag 0; toBuf b fc; toBuf b name; toBuf b idx; toBuf b y
|
||||
TTC Pat where
|
||||
toBuf b (PAs fc x y)
|
||||
= do tag 0; toBuf b fc; toBuf b x; toBuf b y
|
||||
toBuf b (PCon fc x t arity 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)
|
||||
@ -276,16 +275,16 @@ TTC (Pat vars) where
|
||||
= 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 5; toBuf b fc; toBuf b name; toBuf b idx
|
||||
toBuf b (PLoc fc x)
|
||||
= do tag 5; toBuf b fc; toBuf b x
|
||||
toBuf b (PUnmatchable fc x)
|
||||
= do tag 6; toBuf b fc; toBuf b x
|
||||
|
||||
fromBuf r b
|
||||
= case !getTag of
|
||||
0 => do fc <- fromBuf r b; name <- fromBuf r b;
|
||||
idx <- fromBuf r b; y <- fromBuf r b
|
||||
pure (PAs {name} fc idx (mkPrf idx) y)
|
||||
0 => do fc <- fromBuf r b; x <- fromBuf r b;
|
||||
y <- fromBuf r b
|
||||
pure (PAs fc x y)
|
||||
1 => do fc <- fromBuf r b; x <- fromBuf r b
|
||||
t <- fromBuf r b; arity <- fromBuf r b
|
||||
xs <- fromBuf r b
|
||||
@ -299,9 +298,8 @@ TTC (Pat vars) where
|
||||
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))
|
||||
5 => do fc <- fromBuf r b; x <- fromBuf r b
|
||||
pure (PLoc fc x)
|
||||
6 => do fc <- fromBuf r b; x <- fromBuf r b
|
||||
pure (PUnmatchable fc x)
|
||||
_ => corrupt "Pat"
|
||||
|
||||
Loading…
Reference in New Issue
Block a user