edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity

Remove 'Case' from Term structure

Browse Source 
It seems that this isn't going to buy us enough to be worth the
complications of compiling case trees, dealing with 'with' etc.
This commit is contained in:
Edwin Brady 2019-04-19 20:10:55 +01:00
parent 0c7ef9bbac
commit cd958bd304
12 changed files with 463 additions and 895 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Core/CaseBuilder.idr Normal file
View File

@ -0,0 +1,8 @@
module Core.CaseBuilder
import Core.Context
import Core.Core
import Core.Normalise
import Core.TT
import Core.Value

90
src/Core/CaseTree.idr Normal file
View File

@ -0,0 +1,90 @@
module Core.CaseTree
import Core.TT
mutual
public export
data CaseTree : List Name -> Type where
Switch : {name : _} ->
(idx : Nat) -> IsVar name idx vars ->
(scTy : Term vars) -> List (CaseAlt vars) ->
CaseTree vars
STerm : Term vars -> CaseTree vars
Unmatched : (msg : String) -> CaseTree vars
Impossible : CaseTree vars
public export
data CaseAlt : List Name -> Type where
ConCase : Name -> (tag : Int) -> (args : List Name) ->
CaseTree (args ++ vars) -> CaseAlt vars
ConstCase : Constant -> CaseTree vars -> CaseAlt vars
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
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
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
export
mkPat : Term vars -> Pat vars
mkPat tm = mkPat' [] tm tm
mutual
insertCaseNames : (ns : List Name) -> CaseTree (outer ++ inner) ->
CaseTree (outer ++ (ns ++ inner))
insertCaseNames {inner} {outer} ns (Switch idx prf scTy alts)
= let (_ ** prf') = insertVarNames {outer} {inner} {ns} _ prf in
Switch _ prf' (insertNames {outer} ns scTy)
(map (insertCaseAltNames {outer} {inner} ns) alts)
insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x)
insertCaseNames ns (Unmatched msg) = Unmatched msg
insertCaseNames ns Impossible = Impossible
insertCaseAltNames : (ns : List Name) ->
CaseAlt (outer ++ inner) ->
CaseAlt (outer ++ (ns ++ inner))
insertCaseAltNames {outer} {inner} ns (ConCase x tag args ct)
= ConCase x tag args
(rewrite appendAssociative args outer (ns ++ inner) in
insertCaseNames {outer = args ++ outer} {inner} ns
(rewrite sym (appendAssociative args outer inner) in
ct))
insertCaseAltNames ns (ConstCase x ct)
= ConstCase x (insertCaseNames ns ct)
insertCaseAltNames ns (DefaultCase ct)
= DefaultCase (insertCaseNames ns ct)
export
thinTree : (n : Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ n :: inner)
thinTree n (Switch idx prf scTy alts)
= let (_ ** prf') = insertVar {n} _ prf in
Switch _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
thinTree n (STerm tm) = STerm (thin n tm)
thinTree n (Unmatched msg) = Unmatched msg
thinTree n Impossible = Impossible

86
src/Core/Context.idr
View File

@ -242,6 +242,11 @@ data DataDef : Type where
MkData : (tycon : Constructor) -> (datacons : List Constructor) ->
DataDef
public export
data Clause : Type where
MkClause : (env : Env Term vars) ->
(lhs : Term vars) -> (rhs : Term vars) -> Clause
public export
data TotalReq = Total | CoveringOnly | PartialOK
@ -527,67 +532,26 @@ toFullNames tm
= do defs <- get Ctxt
full (gamma defs) tm
where
mutual
full : Context GlobalDef -> Term vars -> Core (Term vars)
full gam (Ref fc x (Resolved i))
= do let a = content gam
arr <- get Arr
Just gdef <- coreLift (readArray arr i)
| Nothing => pure (Ref fc x (Resolved i))
pure (Ref fc x (fullname gdef))
full gam (Meta fc x y xs)
= pure (Meta fc x y !(traverse (full gam) xs))
full gam (Bind fc x b scope)
= pure (Bind fc x !(traverse (full gam) b) !(full gam scope))
full gam (App fc fn p arg)
= pure (App fc !(full gam fn) p !(full gam arg))
full gam (Case fc cs ty Nothing alts)
= pure (Case fc cs !(full gam ty) Nothing
!(traverse (fullPatAlt gam) alts))
full gam (Case fc cs ty (Just t) alts)
= pure (Case fc cs !(full gam ty) (Just !(fullTree gam t))
!(traverse (fullPatAlt gam) alts))
full gam (TDelayed fc x y)
= pure (TDelayed fc x !(full gam y))
full gam (TDelay fc x y)
= pure (TDelay fc x !(full gam y))
full gam (TForce fc x)
= pure (TForce fc !(full gam x))
full gam tm = pure tm
fullPat : Context GlobalDef -> Pat vars -> Core (Pat vars)
fullPat gam (PAs fc idx x y)
= 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)
= pure (PUnmatchable fc !(full gam x))
fullPatAlt : Context GlobalDef -> PatAlt vars -> Core (PatAlt vars)
fullPatAlt gam (CBind c x ty alt)
= pure (CBind c x !(full gam ty) !(fullPatAlt gam alt))
fullPatAlt gam (CPats xs x)
= pure (CPats !(traverse (fullPat gam) xs) !(full gam x))
fullTree : Context GlobalDef -> CaseTree vars -> Core (CaseTree vars)
fullTree gam (Switch idx x scTy xs)
= pure (Switch idx x !(full gam scTy) !(traverse (fullAlt gam) xs))
fullTree gam (STerm x) = pure (STerm !(full gam x))
fullTree gam t = pure t
fullAlt : Context GlobalDef -> CaseAlt vars -> Core (CaseAlt vars)
fullAlt gam (ConCase x tag args t)
= pure (ConCase x tag args !(fullTree gam t))
fullAlt gam (ConstCase x t) = pure (ConstCase x !(fullTree gam t))
fullAlt gam (DefaultCase t) = pure (DefaultCase !(fullTree gam t))
full : Context GlobalDef -> Term vars -> Core (Term vars)
full gam (Ref fc x (Resolved i))
= do let a = content gam
arr <- get Arr
Just gdef <- coreLift (readArray arr i)
| Nothing => pure (Ref fc x (Resolved i))
pure (Ref fc x (fullname gdef))
full gam (Meta fc x y xs)
= pure (Meta fc x y !(traverse (full gam) xs))
full gam (Bind fc x b scope)
= pure (Bind fc x !(traverse (full gam) b) !(full gam scope))
full gam (App fc fn p arg)
= pure (App fc !(full gam fn) p !(full gam arg))
full gam (TDelayed fc x y)
= pure (TDelayed fc x !(full gam y))
full gam (TDelay fc x y)
= pure (TDelay fc x !(full gam y))
full gam (TForce fc x)
= pure (TForce fc !(full gam x))
full gam tm = pure tm
-- Log message with a term, translating back to human readable names first
export

10
src/Core/Env.idr
View File

@ -103,3 +103,13 @@ abstractEnvType fc (b :: env) tm
= abstractEnvType fc env (Bind fc _
(Pi (multiplicity b) Explicit (binderType b)) tm)
-- As above, for the corresponding term
export
abstractEnv : FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
abstractEnv fc [] tm = tm
abstractEnv fc (Let c val ty :: env) tm
= abstractEnv fc env (Bind fc _ (Let c val ty) tm)
abstractEnv fc (b :: env) tm
= abstractEnv fc env (Bind fc _
(Lam (multiplicity b) Explicit (binderType b)) tm)

26
src/Core/Hash.idr
View File

@ -1,5 +1,6 @@
module Core.Hash
import Core.CaseTree
import Core.TT
import Data.List
@ -107,23 +108,20 @@ mutual
= h `hashWithSalt` 3 `hashWithSalt` b `hashWithSalt` scope
hashWithSalt h (App fc fn p arg)
= h `hashWithSalt` 4 `hashWithSalt` fn `hashWithSalt` arg
hashWithSalt h (Case fc cs ty tree alts)
= h `hashWithSalt` 5 `hashWithSalt` cs `hashWithSalt` ty
`hashWithSalt` tree `hashWithSalt` alts
hashWithSalt h (As fc idx y tm)
= h `hashWithSalt` 6 `hashWithSalt` idx `hashWithSalt` tm
= h `hashWithSalt` 5 `hashWithSalt` idx `hashWithSalt` tm
hashWithSalt h (TDelayed fc x y)
= h `hashWithSalt` 8 `hashWithSalt` y
= h `hashWithSalt` 6 `hashWithSalt` y
hashWithSalt h (TDelay fc x y)
= h `hashWithSalt` 8 `hashWithSalt` y
= h `hashWithSalt` 7 `hashWithSalt` y
hashWithSalt h (TForce fc x)
= h `hashWithSalt` 9 `hashWithSalt` x
= h `hashWithSalt` 8 `hashWithSalt` x
hashWithSalt h (PrimVal fc c)
= h `hashWithSalt` 10 `hashWithSalt` (show c)
= h `hashWithSalt` 9 `hashWithSalt` (show c)
hashWithSalt h (Erased fc)
= hashWithSalt h 11
= hashWithSalt h 10
hashWithSalt h (TType fc)
= hashWithSalt h 12
= hashWithSalt h 11
export
Hashable (Pat vars) where
@ -142,14 +140,6 @@ mutual
hashWithSalt h (PUnmatchable fc x)
= h `hashWithSalt` 6 `hashWithSalt` x
export
Hashable (PatAlt vars) where
hashWithSalt h (CBind c n ty p)
= h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` n
`hashWithSalt` p
hashWithSalt h (CPats xs x)
= h `hashWithSalt` 1 `hashWithSalt` xs `hashWithSalt` x
export
Hashable (CaseTree vars) where
hashWithSalt h (Switch idx x scTy xs)

2
src/Core/Normalise.idr
View File

@ -60,8 +60,6 @@ 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 (Case fc cs ty x alts) stk
= throw (InternalError "Case evaluator not implemented")
eval env locs (As fc idx p tm) stk = eval env locs tm stk
eval env locs (TDelayed fc r ty) stk
= pure (NDelayed fc r (MkClosure opts locs env ty))

706
src/Core/TT.idr
View File

@ -11,7 +11,6 @@ import Data.Vect
%hide Raw -- from Reflection in the Prelude
%hide Binder
%hide NameType
%hide Case
public export
data NameType : Type where
@ -281,76 +280,33 @@ namespace CList
-- Typechecked terms
-- These are guaranteed to be well-scoped wrt local variables, because they are
-- indexed by the names of local variables in scope
mutual
public export
data LazyReason = LInf | LLazy
public export
data LazyReason = LInf | LLazy
public export
data Term : List Name -> Type where
Local : {name : _} ->
FC -> Maybe RigCount ->
(idx : Nat) -> IsVar name idx vars -> Term vars
Ref : FC -> NameType -> (name : Name) -> Term vars
-- Metavariables and the scope they are applied to
Meta : FC -> Name -> Int -> List (Term vars) -> Term vars
Bind : FC -> (x : Name) ->
(b : Binder (Term vars)) ->
(scope : Term (x :: vars)) -> Term vars
App : FC -> (fn : Term vars) -> (p : AppInfo) -> (arg : Term vars) -> Term vars
Case : FC -> (cs : List (Var vars)) ->
(ty : Term vars) ->
Maybe (CaseTree vars) ->
(alts : List (PatAlt 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
-- Typed laziness annotations
TDelayed : FC -> LazyReason -> Term vars -> Term vars
TDelay : FC -> LazyReason -> Term vars -> Term vars
TForce : FC -> Term vars -> Term vars
PrimVal : FC -> (c : Constant) -> Term vars
Erased : FC -> Term vars
TType : FC -> Term vars
public export
data Pat : List Name -> Type where
PAs : {name : _} ->
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
public export
data PatAlt : List Name -> Type where
CBind : RigCount -> (x : Name) -> (ty : Term vars) ->
PatAlt (x :: vars) -> PatAlt vars
CPats : List (Pat vars) -> (rhs : Term vars) -> PatAlt vars
public export
data CaseTree : List Name -> Type where
Switch : {name : _} ->
(idx : Nat) -> IsVar name idx vars ->
(scTy : Term vars) -> List (CaseAlt vars) ->
CaseTree vars
STerm : Term vars -> CaseTree vars
Unmatched : (msg : String) -> CaseTree vars
Impossible : CaseTree vars
public export
data CaseAlt : List Name -> Type where
ConCase : Name -> (tag : Int) -> (args : List Name) ->
CaseTree (args ++ vars) -> CaseAlt vars
ConstCase : Constant -> CaseTree vars -> CaseAlt vars
DefaultCase : CaseTree vars -> CaseAlt vars
public export
data Term : List Name -> Type where
Local : {name : _} ->
FC -> Maybe RigCount ->
(idx : Nat) -> IsVar name idx vars -> Term vars
Ref : FC -> NameType -> (name : Name) -> Term vars
-- Metavariables and the scope they are applied to
Meta : FC -> Name -> Int -> List (Term vars) -> Term vars
Bind : FC -> (x : Name) ->
(b : Binder (Term vars)) ->
(scope : Term (x :: vars)) -> Term vars
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
-- Typed laziness annotations
TDelayed : FC -> LazyReason -> Term vars -> Term vars
TDelay : FC -> LazyReason -> Term vars -> Term vars
TForce : FC -> Term vars -> Term vars
PrimVal : FC -> (c : Constant) -> Term vars
Erased : FC -> Term vars
TType : FC -> Term vars
export
getLoc : Term vars -> FC
@ -359,7 +315,6 @@ 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
@ -458,6 +413,7 @@ interface Weaken (tm : List Name -> Type) where
weaken = weakenNs [_]
export
insertVar : {outer : _} ->
(idx : _) ->
IsVar name idx (outer ++ inner) ->
@ -486,153 +442,62 @@ insertVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
= let (_ ** prf) = insertVarNames {ns} i x in
(_ ** Later prf)
mutual
export
thin : {outer, inner : _} ->
(n : Name) -> Term (outer ++ inner) -> Term (outer ++ n :: inner)
thin n (Local fc r idx prf)
= let (idx' ** var') = insertVar {n} idx prf in
Local fc r idx' var'
thin n (Ref fc nt name) = Ref fc nt name
thin n (Meta fc name idx args) = Meta fc name idx (map (thin n) args)
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 {outer} {inner} n (Case fc cs ty tree alts)
= Case fc (map (thinVar {outer} {inner} n) cs)
(thin {outer} {inner} n ty)
(map (thinTree n) tree)
(map (thinPatAlt n) alts)
thin n (As fc idx prf tm)
= let (_ ** prf') = insertVar {n} _ prf in
As fc _ prf' (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)
thin n (PrimVal fc c) = PrimVal fc c
thin n (Erased fc) = Erased fc
thin n (TType fc) = TType fc
export
insertNames : {outer, inner : _} ->
(ns : List Name) -> Term (outer ++ inner) ->
Term (outer ++ (ns ++ inner))
insertNames ns (Local fc r idx prf)
= let (_ ** prf') = insertVarNames {ns} idx prf in
Local fc r _ prf'
insertNames ns (Ref fc nt name) = Ref fc nt name
insertNames ns (Meta fc name idx args)
= Meta fc name idx (map (insertNames ns) args)
insertNames {outer} {inner} ns (Bind fc x b scope)
= Bind fc x (assert_total (map (insertNames ns) b))
(insertNames {outer = x :: outer} {inner} ns scope)
insertNames ns (App fc fn p arg)
= App fc (insertNames ns fn) p (insertNames ns arg)
insertNames {outer} {inner} ns (Case fc cs ty tree alts)
= Case fc (map (insertNamesVar {outer} {inner} ns) cs)
(insertNames ns ty)
(map (insertCaseNames ns) tree)
(map (insertPatAltNames ns) alts)
insertNames ns (As fc idx prf tm)
= let (_ ** prf') = insertVarNames {ns} idx prf in
As fc _ prf' (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)
insertNames ns (PrimVal fc c) = PrimVal fc c
insertNames ns (Erased fc) = Erased fc
insertNames ns (TType fc) = TType fc
export
thin : {outer, inner : _} ->
(n : Name) -> Term (outer ++ inner) -> Term (outer ++ n :: inner)
thin n (Local fc r idx prf)
= let (idx' ** var') = insertVar {n} idx prf in
Local fc r idx' var'
thin n (Ref fc nt name) = Ref fc nt name
thin n (Meta fc name idx args) = Meta fc name idx (map (thin n) args)
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 (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)
thin n (PrimVal fc c) = PrimVal fc c
thin n (Erased fc) = Erased fc
thin n (TType fc) = TType fc
insertCaseNames : (ns : List Name) -> CaseTree (outer ++ inner) ->
CaseTree (outer ++ (ns ++ inner))
insertCaseNames {inner} {outer} ns (Switch idx prf scTy alts)
= let (_ ** prf') = insertVarNames {outer} {inner} {ns} _ prf in
Switch _ prf' (insertNames {outer} ns scTy)
(map (insertCaseAltNames {outer} {inner} ns) alts)
insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x)
insertCaseNames ns (Unmatched msg) = Unmatched msg
insertCaseNames ns Impossible = Impossible
insertCaseAltNames : (ns : List Name) ->
CaseAlt (outer ++ inner) ->
CaseAlt (outer ++ (ns ++ inner))
insertCaseAltNames {outer} {inner} ns (ConCase x tag args ct)
= ConCase x tag args
(rewrite appendAssociative args outer (ns ++ inner) in
insertCaseNames {outer = args ++ outer} {inner} ns
(rewrite sym (appendAssociative args outer inner) in
ct))
insertCaseAltNames ns (ConstCase x ct)
= ConstCase x (insertCaseNames ns ct)
insertCaseAltNames ns (DefaultCase ct)
= DefaultCase (insertCaseNames ns ct)
export
insertNames : {outer, inner : _} ->
(ns : List Name) -> Term (outer ++ inner) ->
Term (outer ++ (ns ++ inner))
insertNames ns (Local fc r idx prf)
= let (_ ** prf') = insertVarNames {ns} idx prf in
Local fc r _ prf'
insertNames ns (Ref fc nt name) = Ref fc nt name
insertNames ns (Meta fc name idx args)
= Meta fc name idx (map (insertNames ns) args)
insertNames {outer} {inner} ns (Bind fc x b scope)
= Bind fc x (assert_total (map (insertNames ns) b))
(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 (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)
insertNames ns (PrimVal fc c) = PrimVal fc c
insertNames ns (Erased fc) = Erased fc
insertNames ns (TType fc) = TType fc
thinVar : (n : Name) -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
thinVar n (MkVar prf)
= let (_ ** prf') = insertVar {n} _ prf in
MkVar prf'
thinVar : (n : Name) -> Var (outer ++ inner) -> Var (outer ++ n :: inner)
thinVar n (MkVar prf)
= let (_ ** prf') = insertVar {n} _ prf in
MkVar prf'
insertNamesVar : (ns : List Name) -> Var (outer ++ inner) -> Var (outer ++ (ns ++ inner))
insertNamesVar ns (MkVar prf)
= let (_ ** prf') = insertVarNames {ns} _ prf in
MkVar prf'
thinTree : (n : Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ n :: inner)
thinTree n (Switch idx prf scTy alts)
= let (_ ** prf') = insertVar {n} _ prf in
Switch _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
thinTree n (STerm tm) = STerm (thin n tm)
thinTree n (Unmatched msg) = Unmatched msg
thinTree n Impossible = Impossible
thinPat : (n : Name) -> Pat (outer ++ inner) -> Pat (outer ++ n :: inner)
thinPat n (PAs fc idx prf p)
= let (_ ** prf') = insertVar {n} _ prf in
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'
thinPat n (PUnmatchable fc tm) = PUnmatchable fc (thin n tm)
insertPatNames : (ns : List Name) ->
Pat (outer ++ inner) -> Pat (outer ++ (ns ++ inner))
insertPatNames ns (PAs fc idx prf p)
= let (_ ** prf') = insertVarNames {ns} _ prf in
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'
insertPatNames ns (PUnmatchable fc tm)
= PUnmatchable fc (insertNames ns tm)
thinPatAlt : (n : Name) -> PatAlt (outer ++ inner) -> PatAlt (outer ++ n :: inner)
thinPatAlt {outer} n (CBind r x ty alt)
= CBind r x (thin n ty) (thinPatAlt {outer = x :: outer} n alt)
thinPatAlt n (CPats pats tm)
= CPats (map (thinPat n) pats) (thin n tm)
insertPatAltNames : (ns : List Name) ->
PatAlt (outer ++ inner) -> PatAlt (outer ++ (ns ++ inner))
insertPatAltNames {outer} ns (CBind r x ty alt)
= CBind r x (insertNames ns ty) (insertPatAltNames {outer = x :: outer} ns alt)
insertPatAltNames ns (CPats pats tm)
= CPats (map (insertPatNames ns) pats) (insertNames ns tm)
insertNamesVar : (ns : List Name) -> Var (outer ++ inner) -> Var (outer ++ (ns ++ inner))
insertNamesVar ns (MkVar prf)
= let (_ ** prf') = insertVarNames {ns} _ prf in
MkVar prf'
export
Weaken Term where
@ -669,70 +534,27 @@ renameLocalRef (CompatExt y) (Later p)
renameVarList : CompatibleVars xs ys -> Var xs -> Var ys
renameVarList prf (MkVar p) = MkVar (snd (renameLocalRef prf p))
mutual
-- TODO: Surely identity at run time, can we replace with 'believe_me'?
export
renameVars : CompatibleVars xs ys -> Term xs -> Term ys
renameVars CompatPre tm = tm
renameVars prf (Local fc r idx vprf)
= Local fc r idx (snd (renameLocalRef prf vprf))
renameVars prf (Ref fc x name) = Ref fc x name
renameVars prf (Meta fc n i args)
= Meta fc n i (map (renameVars prf) args)
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 (Case fc cs ty tree alts)
= Case fc (map (renameVarList prf) cs) (renameVars prf ty)
(map (renameTree prf) tree)
(map (renamePatAlt prf) alts)
renameVars prf (As fc idx vprf tm)
= As fc idx (snd (renameLocalRef prf vprf)) (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)
renameVars prf (PrimVal fc c) = PrimVal fc c
renameVars prf (Erased fc) = Erased fc
renameVars prf (TType fc) = TType fc
renameCaseAlt : CompatibleVars xs ys -> CaseAlt xs -> CaseAlt ys
renameCaseAlt prf (ConCase x tag args tree)
= ConCase x tag args (renameTree (extendCompats args prf) tree)
renameCaseAlt prf (ConstCase c tree)
= ConstCase c (renameTree prf tree)
renameCaseAlt prf (DefaultCase tree)
= DefaultCase (renameTree prf tree)
renameTree : CompatibleVars xs ys -> CaseTree xs -> CaseTree ys
renameTree prf (Switch idx x scTy xs)
= Switch idx (snd (renameLocalRef prf x)) (renameVars prf scTy)
(map (renameCaseAlt prf) xs)
renameTree prf (STerm tm) = STerm (renameVars prf tm)
renameTree prf (Unmatched msg) = Unmatched msg
renameTree prf Impossible = Impossible
renamePat : CompatibleVars xs ys -> Pat xs -> Pat ys
renamePat prf (PAs fc idx p pat)
= 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)
= PUnmatchable fc (renameVars prf tm)
renamePatAlt : CompatibleVars xs ys -> PatAlt xs -> PatAlt ys
renamePatAlt prf (CBind r x ty alt)
= CBind r x (renameVars prf ty) (renamePatAlt (CompatExt prf) alt)
renamePatAlt prf (CPats xs tm)
= CPats (map (renamePat prf) xs) (renameVars prf tm)
-- TODO: Surely identity at run time, can we replace with 'believe_me'?
export
renameVars : CompatibleVars xs ys -> Term xs -> Term ys
renameVars CompatPre tm = tm
renameVars prf (Local fc r idx vprf)
= Local fc r idx (snd (renameLocalRef prf vprf))
renameVars prf (Ref fc x name) = Ref fc x name
renameVars prf (Meta fc n i args)
= Meta fc n i (map (renameVars prf) args)
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 (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)
renameVars prf (PrimVal fc c) = PrimVal fc c
renameVars prf (Erased fc) = Erased fc
renameVars prf (TType fc) = TType fc
export
renameTop : (m : Name) -> Term (n :: vars) -> Term (m :: vars)
@ -784,61 +606,6 @@ mutual
Nothing => Nothing
Just (_ ** x') => Just (MkVar x')
export
shrinkTree : CaseTree vars -> SubVars newvars vars -> Maybe (CaseTree newvars)
shrinkTree (Switch idx x scTy xs) prf
= case subElem x prf of
Nothing => Nothing
Just (_ ** x') =>
Just (Switch _ x' !(shrinkTerm scTy prf)
!(traverse (\x => shrinkCaseAlt x prf) xs))
shrinkTree (STerm x) prf = Just (STerm !(shrinkTerm x prf))
shrinkTree (Unmatched msg) prf = Just (Unmatched msg)
shrinkTree Impossible prf = Just Impossible
export
shrinkCaseAlt : CaseAlt vars -> SubVars newvars vars -> Maybe (CaseAlt newvars)
shrinkCaseAlt (ConCase x tag args tree) prf
= Just (ConCase x tag args !(shrinkTree tree (keepArgs args prf)))
where
keepArgs : (args : List Name) ->
SubVars newvars vars -> SubVars (args ++ newvars) (args ++ vars)
keepArgs [] prf = prf
keepArgs (x :: xs) prf = KeepCons (keepArgs xs prf)
shrinkCaseAlt (ConstCase x tree) prf
= Just (ConstCase x !(shrinkTree tree prf))
shrinkCaseAlt (DefaultCase tree) prf
= Just (DefaultCase !(shrinkTree tree prf))
export
shrinkPatAlt : PatAlt vars -> SubVars newvars vars -> Maybe (PatAlt newvars)
shrinkPatAlt (CBind r x ty alt) prf
= Just (CBind r x !(shrinkTerm ty prf) !(shrinkPatAlt alt (KeepCons prf)))
shrinkPatAlt (CPats xs tm) prf
= Just (CPats !(traverse (\x => shrinkPat x prf) xs)
!(shrinkTerm tm prf))
shrinkPat : Pat vars -> SubVars newvars vars -> Maybe (Pat newvars)
shrinkPat (PAs fc idx x pat) prf
= case subElem x prf of
Nothing => Nothing
Just (_ ** x') =>
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
Just (_ ** x') =>
Just (PLoc fc _ x')
shrinkPat (PUnmatchable fc x) prf
= Just (PUnmatchable fc !(shrinkTerm x prf))
export
shrinkTerm : Term vars -> SubVars newvars vars -> Maybe (Term newvars)
shrinkTerm (Local fc r idx loc) prf
@ -853,11 +620,6 @@ 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 (Case fc cs ty tree alts) prf
= Just (Case fc !(traverse (\x => shrinkVar x prf) cs)
!(shrinkTerm ty prf)
!(traverse (\x => shrinkTree x prf) tree)
!(traverse (\x => shrinkPatAlt x prf) alts))
shrinkTerm (As fc idx loc tm) prf
= case subElem loc prf of
Nothing => Nothing
@ -910,218 +672,91 @@ resolveRef {later} {vars} done (Add {xs} new old bs) fc n
else rewrite appendAssociative done [new] (xs ++ vars)
in resolveRef (done ++ [new]) bs fc n
mutual
mkLocalVar : {later, bound : _} ->
Bounds bound ->
Var (later ++ vars) -> Var (later ++ (bound ++ vars))
mkLocalVar bs (MkVar p)
= let (_ ** p') = addVars bs p in MkVar p'
mkLocalTree : {later, bound : _} ->
Bounds bound ->
CaseTree (later ++ vars) -> CaseTree (later ++ (bound ++ vars))
mkLocalTree bs (Switch idx p scTy alts)
= let (_ ** p') = addVars bs p in
Switch _ p' (mkLocals bs scTy) (map (mkLocalCaseAlt bs) alts)
mkLocalTree bs (STerm tm) = STerm (mkLocals bs tm)
mkLocalTree bs (Unmatched msg) = Unmatched msg
mkLocalTree bs Impossible = Impossible
mkLocalCaseAlt : {later, bound : _} ->
Bounds bound ->
CaseAlt (later ++ vars) -> CaseAlt (later ++ (bound ++ vars))
mkLocalCaseAlt {later} {vars} {bound} bs (ConCase x tag args t)
= ConCase x tag args
(let t' = mkLocalTree {later = args ++ later} {vars} bs
(rewrite sym (appendAssociative args later vars) in t)
in rewrite appendAssociative args later (bound ++ vars)
in t')
mkLocalCaseAlt bs (ConstCase c t) = ConstCase c (mkLocalTree bs t)
mkLocalCaseAlt bs (DefaultCase t) = DefaultCase (mkLocalTree bs t)
mkLocalPat : {later, bound : _} ->
Bounds bound ->
Pat (later ++ vars) -> Pat (later ++ (bound ++ vars))
mkLocalPat bs (PAs fc idx p pat)
= let (_ ** p') = addVars bs p in
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'
mkLocalPat bs (PUnmatchable fc x) = PUnmatchable fc (mkLocals bs x)
mkLocalPatAlt : {later, bound : _} ->
Bounds bound ->
PatAlt (later ++ vars) -> PatAlt (later ++ (bound ++ vars))
mkLocalPatAlt {later} bs (CBind c n ty sc)
= CBind c n (mkLocals bs ty)
(mkLocalPatAlt {later = n :: later} bs sc)
mkLocalPatAlt bs (CPats xs rhs)
= CPats (map (mkLocalPat bs) xs) (mkLocals bs rhs)
mkLocals : {later, bound : _} ->
mkLocalVar : {later, bound : _} ->
Bounds bound ->
Term (later ++ vars) -> Term (later ++ (bound ++ vars))
mkLocals bs (Local fc r idx p)
= let (_ ** p') = addVars bs p in Local fc r _ p'
mkLocals bs (Ref fc Bound name)
= maybe (Ref fc Bound name) id (resolveRef [] bs fc name)
mkLocals bs (Ref fc nt name)
= Ref fc nt name
mkLocals bs (Meta fc name y xs)
= maybe (Meta fc name y (map (mkLocals bs) xs))
id (resolveRef [] bs fc name)
mkLocals {later} bs (Bind fc x b scope)
= Bind fc x (map (mkLocals bs) b)
(mkLocals {later = x :: later} bs scope)
mkLocals bs (App fc fn p arg)
= App fc (mkLocals bs fn) p (mkLocals bs arg)
mkLocals bs (Case fc cs ty tree alts)
= Case fc (map (mkLocalVar bs) cs) (mkLocals bs ty)
(map (mkLocalTree bs) tree) (map (mkLocalPatAlt bs) alts)
mkLocals bs (As fc idx p tm)
= let (_ ** p') = addVars bs p in As fc _ p' (mkLocals bs tm)
mkLocals bs (TDelayed fc x y)
= TDelayed fc x (mkLocals bs y)
mkLocals bs (TDelay fc x y)
= TDelay fc x (mkLocals bs y)
mkLocals bs (TForce fc x)
= TForce fc (mkLocals bs x)
mkLocals bs (PrimVal fc c) = PrimVal fc c
mkLocals bs (Erased fc) = Erased fc
mkLocals bs (TType fc) = TType fc
Var (later ++ vars) -> Var (later ++ (bound ++ vars))
mkLocalVar bs (MkVar p)
= let (_ ** p') = addVars bs p in MkVar p'
mkLocals : {later, bound : _} ->
Bounds bound ->
Term (later ++ vars) -> Term (later ++ (bound ++ vars))
mkLocals bs (Local fc r idx p)
= let (_ ** p') = addVars bs p in Local fc r _ p'
mkLocals bs (Ref fc Bound name)
= maybe (Ref fc Bound name) id (resolveRef [] bs fc name)
mkLocals bs (Ref fc nt name)
= Ref fc nt name
mkLocals bs (Meta fc name y xs)
= maybe (Meta fc name y (map (mkLocals bs) xs))
id (resolveRef [] bs fc name)
mkLocals {later} bs (Bind fc x b scope)
= Bind fc x (map (mkLocals bs) b)
(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 (TDelayed fc x y)
= TDelayed fc x (mkLocals bs y)
mkLocals bs (TDelay fc x y)
= TDelay fc x (mkLocals bs y)
mkLocals bs (TForce fc x)
= TForce fc (mkLocals bs x)
mkLocals bs (PrimVal fc c) = PrimVal fc c
mkLocals bs (Erased fc) = Erased fc
mkLocals bs (TType fc) = TType fc
export
refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
refsToLocals bs y = mkLocals {later = []} bs y
-- Get the metavariable names in a term
-- TODO: There's a lot of boilerplate and repetition in what follows, so
-- tidying it up would be nice
export
getMetas : Term vars -> NameMap ()
getMetas tm = getMap empty tm
where
mutual
getMap : NameMap () -> Term vars -> NameMap ()
getMap ns (Local fc x idx y) = ns
getMap ns (Ref fc x name) = ns
getMap ns (Meta fc n i xs) = insert n () ns
getMap ns (Bind fc x (Let c val ty) scope)
= getMap (getMap (getMap ns val) ty) scope
getMap ns (Bind fc x b scope)
= getMap (getMap ns (binderType b)) scope
getMap ns (App fc fn p arg)
= getMap (getMap ns fn) arg
getMap ns (Case fc cs ty tree alts)
= let nst = maybe ns (getTreeMap ns) tree in
getAll getAltMap (getMap nst ty) alts
getMap ns (As fc idx x y) = getMap ns y
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
getMap ns (PrimVal fc c) = ns
getMap ns (Erased fc) = ns
getMap ns (TType fc) = ns
getMap : NameMap () -> Term vars -> NameMap ()
getMap ns (Local fc x idx y) = ns
getMap ns (Ref fc x name) = ns
getMap ns (Meta fc n i xs) = insert n () ns
getMap ns (Bind fc x (Let c val ty) scope)
= getMap (getMap (getMap ns val) ty) scope
getMap ns (Bind fc x b scope)
= 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 (TDelayed fc x y) = getMap ns y
getMap ns (TDelay fc x y) = getMap ns y
getMap ns (TForce fc x) = getMap ns x
getMap ns (PrimVal fc c) = ns
getMap ns (Erased fc) = ns
getMap ns (TType fc) = ns
getAll : (NameMap () -> a -> NameMap ()) ->
NameMap () -> List a -> NameMap ()
getAll f ns [] = ns
getAll f ns (x :: xs)
= getAll f (f ns x) xs
getTreeMap : NameMap () -> CaseTree vars -> NameMap ()
getTreeMap ns (Switch idx x scTy alts)
= getAll getCaseAltMap (getMap ns scTy) alts
getTreeMap ns (STerm x) = getMap ns x
getTreeMap ns (Unmatched msg) = ns
getTreeMap ns Impossible = ns
getCaseAltMap : NameMap () -> CaseAlt vars -> NameMap ()
getCaseAltMap ns (ConCase x tag args t) = getTreeMap ns t
getCaseAltMap ns (ConstCase x t) = getTreeMap ns t
getCaseAltMap ns (DefaultCase t) = getTreeMap ns t
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
getAltMap : NameMap () -> PatAlt vars -> NameMap ()
getAltMap ns (CBind x y ty alt) = getAltMap (getMap ns ty) alt
getAltMap ns (CPats xs rhs) = getMap ns rhs
-- As above, but for references (and see also the TODO about boilerplate!
-- The only difference is between the 'Ref' and 'Meta' cases)
-- As above, but for references (the only difference is between the 'Ref' and
-- 'Meta' cases, perhaps refector a bit?)
export
getRefs : Term vars -> NameMap ()
getRefs tm = getMap empty tm
where
mutual
getMap : NameMap () -> Term vars -> NameMap ()
getMap ns (Local fc x idx y) = ns
getMap ns (Ref fc x name) = insert name () ns
getMap ns (Meta fc n i xs) = ns
getMap ns (Bind fc x (Let c val ty) scope)
= getMap (getMap (getMap ns val) ty) scope
getMap ns (Bind fc x b scope)
= getMap (getMap ns (binderType b)) scope
getMap ns (App fc fn p arg)
= getMap (getMap ns fn) arg
getMap ns (Case fc cs ty tree alts)
= let nst = maybe ns (getTreeMap ns) tree in
getAll getAltMap (getMap nst ty) alts
getMap ns (As fc idx x y) = getMap ns y
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
getMap ns (PrimVal fc c) = ns
getMap ns (Erased fc) = ns
getMap ns (TType fc) = ns
getAll : (NameMap () -> a -> NameMap ()) ->
NameMap () -> List a -> NameMap ()
getAll f ns [] = ns
getAll f ns (x :: xs)
= getAll f (f ns x) xs
getTreeMap : NameMap () -> CaseTree vars -> NameMap ()
getTreeMap ns (Switch idx x scTy alts)
= getAll getCaseAltMap (getMap ns scTy) alts
getTreeMap ns (STerm x) = getMap ns x
getTreeMap ns (Unmatched msg) = ns
getTreeMap ns Impossible = ns
getCaseAltMap : NameMap () -> CaseAlt vars -> NameMap ()
getCaseAltMap ns (ConCase x tag args t) = getTreeMap ns t
getCaseAltMap ns (ConstCase x t) = getTreeMap ns t
getCaseAltMap ns (DefaultCase t) = getTreeMap ns t
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
getAltMap : NameMap () -> PatAlt vars -> NameMap ()
getAltMap ns (CBind x y ty alt) = getAltMap (getMap ns ty) alt
getAltMap ns (CPats xs rhs) = getMap ns rhs
getMap : NameMap () -> Term vars -> NameMap ()
getMap ns (Local fc x idx y) = ns
getMap ns (Ref fc x name) = insert name () ns
getMap ns (Meta fc n i xs) = ns
getMap ns (Bind fc x (Let c val ty) scope)
= getMap (getMap (getMap ns val) ty) scope
getMap ns (Bind fc x b scope)
= 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 (TDelayed fc x y) = getMap ns y
getMap ns (TDelay fc x y) = getMap ns y
getMap ns (TForce fc x) = getMap ns x
getMap ns (PrimVal fc c) = ns
getMap ns (Erased fc) = ns
getMap ns (TType fc) = ns
export Show (Term vars) where
show tm = let (fn, args) = getFnArgs tm in showApp fn args
@ -1155,7 +790,6 @@ export Show (Term vars) where
= "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++
" => " ++ show sc
showApp (App _ _ _ _) [] = "[can't happen]"
showApp (Case _ _ _ _ _) [] = "[case tree]"
showApp (TDelayed _ _ tm) [] = "Delayed " ++ show tm
showApp (TDelay _ _ tm) [] = "Delay " ++ show tm
showApp (TForce _ tm) [] = "Force " ++ show tm

252
src/Core/TTC.idr
View File

@ -1,5 +1,6 @@
module Core.TTC
import Core.CaseTree
import Core.Core
import Core.Env
import Core.FC
@ -191,144 +192,121 @@ TTC (Var vars) where
i <- fromBuf r b
pure (MkVar {n} (mkPrf i))
export
TTC (Term vars) where
toBuf b (Local {name} fc c idx y)
= do tag 0;
toBuf b fc; toBuf b name
toBuf b c; toBuf b idx
toBuf b (Ref fc nt name)
= do tag 1;
toBuf b fc; toBuf b nt; toBuf b name
toBuf b (Meta fc n i xs)
= do tag 2;
toBuf b fc; toBuf b n; toBuf b i; toBuf b xs
toBuf b (Bind fc x bnd scope)
= do tag 3;
toBuf b fc; toBuf b bnd; toBuf b scope
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)
= do tag 5;
toBuf b fc; toBuf b name;
toBuf b idx; toBuf b tm
toBuf b (TDelayed fc r tm)
= do tag 6;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TDelay fc r tm)
= do tag 7;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TForce fc tm)
= do tag 8;
toBuf b fc; toBuf b tm
toBuf b (PrimVal fc c)
= do tag 9;
toBuf b fc; toBuf b c
toBuf b (Erased fc)
= do tag 10;
toBuf b fc
toBuf b (TType fc)
= do tag 11;
toBuf b fc
fromBuf r b
= case !getTag of
0 => do fc <- fromBuf r b; name <- fromBuf r b
c <- fromBuf r b; idx <- fromBuf r b
pure (Local {name} fc c idx (mkPrf idx))
1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b
pure (Ref fc nt name)
2 => do fc <- fromBuf r b; n <- fromBuf r b; i <- fromBuf r b
xs <- fromBuf r b
pure (Meta fc n i xs)
3 => do fc <- fromBuf r b; x <- fromBuf r b
bnd <- fromBuf r b; scope <- fromBuf r b
pure (Bind fc x bnd scope)
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)
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
pure (TDelay fc lr tm)
8 => do fc <- fromBuf r b; tm <- fromBuf r b
pure (TForce fc tm)
9 => do fc <- fromBuf r b; c <- fromBuf r b
pure (PrimVal fc c)
10 => do fc <- fromBuf r b; pure (Erased fc)
11 => do fc <- fromBuf r b; pure (TType fc)
_ => 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
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)
= 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 5; toBuf b fc; toBuf b name; toBuf b idx
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)
1 => do fc <- fromBuf r b; x <- fromBuf r b
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; 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))
6 => do fc <- fromBuf r b; x <- fromBuf r b
pure (PUnmatchable fc x)
_ => corrupt "Pat"
mutual
export
TTC (Term vars) where
toBuf b (Local {name} fc c idx y)
= do tag 0;
toBuf b fc; toBuf b name
toBuf b c; toBuf b idx
toBuf b (Ref fc nt name)
= do tag 1;
toBuf b fc; toBuf b nt; toBuf b name
toBuf b (Meta fc n i xs)
= do tag 2;
toBuf b fc; toBuf b n; toBuf b i; toBuf b xs
toBuf b (Bind fc x bnd scope)
= do tag 3;
toBuf b fc; toBuf b bnd; toBuf b scope
toBuf b (App fc fn p arg)
= do tag 4;
toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg
toBuf b (Case fc cs ty tree alts)
= do tag 5;
toBuf b fc; toBuf b cs; toBuf b ty; toBuf b tree; toBuf b alts
toBuf b (As {name} fc idx p tm)
= do tag 6;
toBuf b fc; toBuf b name;
toBuf b idx; toBuf b tm
toBuf b (TDelayed fc r tm)
= do tag 7;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TDelay fc r tm)
= do tag 8;
toBuf b fc; toBuf b r; toBuf b tm
toBuf b (TForce fc tm)
= do tag 9;
toBuf b fc; toBuf b tm
toBuf b (PrimVal fc c)
= do tag 10;
toBuf b fc; toBuf b c
toBuf b (Erased fc)
= do tag 11;
toBuf b fc
toBuf b (TType fc)
= do tag 12;
toBuf b fc
fromBuf r b
= case !getTag of
0 => do fc <- fromBuf r b; name <- fromBuf r b
c <- fromBuf r b; idx <- fromBuf r b
pure (Local {name} fc c idx (mkPrf idx))
1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b
pure (Ref fc nt name)
2 => do fc <- fromBuf r b; n <- fromBuf r b; i <- fromBuf r b
xs <- fromBuf r b
pure (Meta fc n i xs)
3 => do fc <- fromBuf r b; x <- fromBuf r b
bnd <- fromBuf r b; scope <- fromBuf r b
pure (Bind fc x bnd scope)
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; cs <- fromBuf r b
ty <- fromBuf r b; tree <- fromBuf r b
alts <- fromBuf r b
pure (Case fc cs ty tree alts)
6 => 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)
7 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
pure (TDelayed fc lr tm)
8 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
pure (TDelay fc lr tm)
9 => do fc <- fromBuf r b; tm <- fromBuf r b
pure (TForce fc tm)
10 => do fc <- fromBuf r b; c <- fromBuf r b
pure (PrimVal fc c)
11 => do fc <- fromBuf r b; pure (Erased fc)
12 => do fc <- fromBuf r b; pure (TType fc)
_ => 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
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)
= 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 5; toBuf b fc; toBuf b name; toBuf b idx
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)
1 => do fc <- fromBuf r b; x <- fromBuf r b
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; 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))
6 => do fc <- fromBuf r b; x <- fromBuf r b
pure (PUnmatchable fc x)
_ => corrupt "Pat"
export
TTC (PatAlt vars) where
toBuf b (CBind c x ty alt)
= do tag 0; toBuf b c; toBuf b x; toBuf b ty; toBuf b alt
toBuf b (CPats xs tm)
= do tag 1; toBuf b xs; toBuf b tm
fromBuf r b
= case !getTag of
0 => do c <- fromBuf r b; x <- fromBuf r b
ty <- fromBuf r b; alt <- fromBuf r b
pure (CBind c x ty alt)
1 => do xs <- fromBuf r b; tm <- fromBuf r b
pure (CPats xs tm)
_ => corrupt "PatAlt"
export
TTC (CaseTree vars) where
toBuf b (Switch {name} idx x scTy xs)

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

@ -42,9 +42,6 @@ mutual
= Bind fc x (map (embedSub sub) b) (embedSub (KeepCons sub) scope)
embedSub sub (App fc fn p arg)
= App fc (embedSub sub fn) p (embedSub sub arg)
embedSub sub (Case fc cs ty tree alts)
= Case fc (map (embedVar sub) cs) (embedSub sub ty)
(map (embedTree sub) tree) (map (embedPatAlt sub) alts)
embedSub sub (As fc idx x y)
= let (_ ** x') = varEmbedSub sub x in
As fc _ x' (embedSub sub y)
@ -55,44 +52,6 @@ mutual
embedSub sub (Erased fc) = Erased fc
embedSub sub (TType fc) = TType fc
embedTree : SubVars small vars -> CaseTree small -> CaseTree vars
embedTree sub (Switch idx x scTy xs)
= let (_ ** x') = varEmbedSub sub x in
Switch _ x' (embedSub sub scTy) (map (embedCaseAlt sub) xs)
embedTree sub (STerm x) = STerm (embedSub sub x)
embedTree sub (Unmatched msg) = Unmatched msg
embedTree sub Impossible = Impossible
embedCaseAlt : SubVars small vars -> CaseAlt small -> CaseAlt vars
embedCaseAlt sub (ConCase x tag args t)
= ConCase x tag args (embedTree (subExtend args sub) t)
embedCaseAlt sub (ConstCase x t) = ConstCase x (embedTree sub t)
embedCaseAlt sub (DefaultCase t) = DefaultCase (embedTree sub t)
embedPat : SubVars small vars -> Pat small -> Pat vars
embedPat sub (PAs fc idx x y)
= let (_ ** x') = varEmbedSub sub x in
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'
embedPat sub (PUnmatchable fc x) = PUnmatchable fc (embedSub sub x)
embedPatAlt : SubVars small vars -> PatAlt small -> PatAlt vars
embedPatAlt sub (CBind c n ty alt)
= CBind c n (embedSub sub ty) (embedPatAlt (KeepCons sub) alt)
embedPatAlt sub (CPats xs rhs)
= CPats (map (embedPat sub) xs) (embedSub sub rhs)
-- Make a hole for an unbound implicit in the outer environment
export
mkOuterHole : {auto e : Ref EST (EState vars)} ->
@ -231,71 +190,23 @@ swapIsVar (x :: xs) First = (_ ** First)
swapIsVar (x :: xs) (Later p)
= let (_ ** p') = swapIsVar xs p in (_ ** Later p')
mutual
swapVars : {vs : List Name} ->
Term (vs ++ x :: y :: ys) -> Term (vs ++ y :: x :: ys)
swapVars (Local fc x idx p)
= let (_ ** p') = swapIsVar _ p in Local fc x _ p'
swapVars (Ref fc x name) = Ref fc x name
swapVars (Meta fc n i xs) = Meta fc n i (map swapVars xs)
swapVars {vs} (Bind fc x b scope)
= Bind fc x (map swapVars b) (swapVars {vs = x :: vs} scope)
swapVars (App fc fn p arg) = App fc (swapVars fn) p (swapVars arg)
swapVars (Case fc cs ty tree alts)
= Case fc (map swapInVar cs) (swapVars ty)
(map swapTree tree) (map swapPatAlt alts)
where
swapInVar : Var (vs ++ x :: y :: ys) -> Var (vs ++ y :: x :: ys)
swapInVar (MkVar p) = let (_ ** p') = swapIsVar _ p in MkVar p'
swapVars (As fc idx p tm)
= let (_ ** p') = swapIsVar _ p in As fc _ p' (swapVars tm)
swapVars (TDelayed fc x tm) = TDelayed fc x (swapVars tm)
swapVars (TDelay fc x tm) = TDelay fc x (swapVars tm)
swapVars (TForce fc tm) = TForce fc (swapVars tm)
swapVars (PrimVal fc c) = PrimVal fc c
swapVars (Erased fc) = Erased fc
swapVars (TType fc) = TType fc
swapTree : {vs : List Name} ->
CaseTree (vs ++ x :: y :: ys) -> CaseTree (vs ++ y :: x :: ys)
swapTree (Switch idx p scTy xs)
= let (_ ** p') = swapIsVar _ p in
Switch _ p' (swapVars scTy) (map swapCaseAlt xs)
swapTree (STerm x) = STerm (swapVars x)
swapTree (Unmatched msg) = Unmatched msg
swapTree Impossible = Impossible
swapCaseAlt : {vs : List Name} ->
CaseAlt (vs ++ x :: y :: ys) -> CaseAlt (vs ++ y :: x :: ys)
swapCaseAlt {vs} {x} {y} {ys} (ConCase n tag args t)
= let t' = swapTree {vs = args ++ vs} {x} {y} {ys}
(rewrite sym (appendAssociative args vs (x :: y :: ys)) in t)
in
ConCase x tag args
(rewrite appendAssociative args vs (y :: x :: ys) in t')
swapCaseAlt (ConstCase c t) = ConstCase c (swapTree t)
swapCaseAlt (DefaultCase t) = DefaultCase (swapTree t)
swapPatAlt : {vs : List Name} ->
PatAlt (vs ++ x :: y :: ys) -> PatAlt (vs ++ y :: x :: ys)
swapPatAlt {vs} (CBind c x ty alt)
= CBind c x (swapVars ty) (swapPatAlt {vs = x :: vs} alt)
swapPatAlt (CPats xs rhs) = CPats (map swapPat xs) (swapVars rhs)
swapPat : {vs : List Name} ->
Pat (vs ++ x :: y :: ys) -> Pat (vs ++ y :: x :: ys)
swapPat (PAs fc idx p pat)
= 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)
swapVars : {vs : List Name} ->
Term (vs ++ x :: y :: ys) -> Term (vs ++ y :: x :: ys)
swapVars (Local fc x idx p)
= let (_ ** p') = swapIsVar _ p in Local fc x _ p'
swapVars (Ref fc x name) = Ref fc x name
swapVars (Meta fc n i xs) = Meta fc n i (map swapVars xs)
swapVars {vs} (Bind fc x b scope)
= Bind fc x (map swapVars b) (swapVars {vs = x :: vs} scope)
swapVars (App fc fn p arg) = App fc (swapVars fn) p (swapVars arg)
swapVars (As fc idx p tm)
= let (_ ** p') = swapIsVar _ p in As fc _ p' (swapVars tm)
swapVars (TDelayed fc x tm) = TDelayed fc x (swapVars tm)
swapVars (TDelay fc x tm) = TDelay fc x (swapVars tm)
swapVars (TForce fc tm) = TForce fc (swapVars tm)
swapVars (PrimVal fc c) = PrimVal fc c
swapVars (Erased fc) = Erased fc
swapVars (TType fc) = TType fc
-- Push an explicit pi binder as far into a term as it'll go. That is,
-- move it under implicit binders that don't depend on it, and stop

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

@ -39,7 +39,6 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamTm tm exp
= case getFn exp of
Ref _ Func _ => pure Nothing -- might still be implicit
Case _ _ _ _ _ => pure Nothing
TForce _ _ => pure Nothing
Bind _ _ (Lam _ _ _) _ => pure Nothing
_ => pure $ Just tm

52
src/TTImp/ProcessDef.idr
View File

@ -1,5 +1,6 @@
module TTImp.ProcessDef
-- import Core.CaseBuilder
import Core.Context
import Core.Core
import Core.Env
@ -11,41 +12,20 @@ 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
Core (vars' ** (Env Term vars', Term vars', Term vars'))
extendEnv env (Bind _ n (PVar c tmty) sc) (Bind _ n' (PVTy _ _) tysc) with (nameEq n n')
extendEnv env (Bind _ n (PVar c tmty) sc) (Bind _ n' (PVTy _ _) tysc) | 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)))
extendEnv env (Bind _ n (PVar c tmty) sc) (Bind _ n (PVTy _ _) tysc) | (Just Refl)
= extendEnv (PVar c tmty :: env) sc tysc
extendEnv env tm ty
= pure (_ ** (env, tm, ty))
-- Find names which are applied to a function in a Rig1/Rig0 position,
-- so that we know how they should be bound on the right hand side of the
@ -143,7 +123,7 @@ checkClause : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(mult : RigCount) -> (hashit : Bool) ->
Name -> Env Term vars ->
ImpClause -> Core (Maybe (PatAlt vars))
ImpClause -> Core (Maybe Clause)
checkClause mult hashit n env (ImpossibleClause fc lhs)
= throw (InternalError "impossible not implemented yet")
checkClause mult hashit n env (PatClause fc lhs_in rhs)
@ -168,13 +148,13 @@ checkClause mult hashit n env (PatClause fc lhs_in rhs)
logTermNF 0 "LHS term" env lhstm_lin
logTermNF 0 "LHS type" env lhsty_lin
(vars' ** (env', lhstm', lhsty', mkAlt)) <-
extendEnv env lhstm_lin lhsty_lin id
(vars' ** (env', lhstm', lhsty')) <-
extendEnv env lhstm_lin lhsty_lin
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))
pure (Just (MkClause env' lhstm' rhstm))
where
noLet : Env Term vs -> Env Term vs
noLet [] = []
@ -186,7 +166,7 @@ processDef : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Env Term vars -> FC ->
Name -> List ImpClause -> Core ()
processDef env fc n_in cs_in
processDef {vars} env fc n_in cs_in
= do n <- inCurrentNS n_in
defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
@ -199,4 +179,8 @@ processDef env fc n_in cs_in
then Rig0
else Rig1
cs <- traverse (checkClause mult hashit n env) cs_in
?something
?foo
-- t <- getCaseTree env ty (mapMaybe id cs)
-- let def = abstractEnv fc env t
-- addDef n (record { definition = Fn def } gdef)
-- pure ()

2
yaffle.ipkg
View File

@ -4,6 +4,8 @@ modules =
Control.Delayed,
Core.Binary,
Core.CaseBuilder,
Core.CaseTree,
Core.Context,
Core.Core,
Core.Env,