184 lines
4.6 KiB
Idris
184 lines
4.6 KiB
Idris
module Quox.Untyped.Erase
|
|
|
|
import Quox.Definition
|
|
import Quox.Syntax.Term.Base as Q
|
|
import Quox.Syntax.Term.Subst
|
|
import Quox.Untyped.Syntax as U
|
|
|
|
import Control.Eff
|
|
|
|
%default total
|
|
|
|
|
|
public export
|
|
data IsErased = Erased | Kept
|
|
|
|
public export
|
|
isErased : Qty -> IsErased
|
|
isErased Zero = Erased
|
|
isErased One = Kept
|
|
isErased Any = Kept
|
|
|
|
|
|
public export
|
|
EContext : Nat -> Type
|
|
EContext = Context' IsErased
|
|
|
|
public export
|
|
record ErasureContext d n where
|
|
constructor MkEContexts
|
|
dnames : Context' Binder d
|
|
tnames : Context' Binder n
|
|
erased : EContext n
|
|
%name ErasureContext ctx
|
|
|
|
|
|
public export
|
|
data Error =
|
|
CompileTimeOnly (ErasureContext d n) (Q.Term d n)
|
|
| Expected String (ErasureContext d n) (Q.Term d n)
|
|
| ErasedVar (ErasureContext d n) (Var n)
|
|
| NotInScope Name
|
|
|
|
public export
|
|
Erase : List (Type -> Type)
|
|
Erase = [Except Error, Reader Definitions]
|
|
|
|
|
|
export
|
|
extendTy : Binder -> Qty -> ErasureContext d n -> ErasureContext d (S n)
|
|
extendTy x pi (MkEContexts dnames tnames erased) =
|
|
MkEContexts dnames (tnames :< x) (erased :< isErased pi)
|
|
|
|
export
|
|
extendDim : Binder -> ErasureContext d n -> ErasureContext (S d) n
|
|
extendDim i (MkEContexts dnames tnames erased) =
|
|
MkEContexts (dnames :< i) tnames erased
|
|
|
|
|
|
private %inline
|
|
(.bname) : Scoped 1 _ _ -> Binder
|
|
t.bname = Bind t.name.val
|
|
|
|
|
|
export covering
|
|
eraseTerm : ErasureContext d n ->
|
|
(ty, tm : Q.Term d n) -> Eff Erase (U.Term n)
|
|
|
|
export covering
|
|
eraseElim : ErasureContext d n -> (tm : Q.Elim d n) -> Eff Erase (U.Term n)
|
|
|
|
eraseTerm ctx _ s@(TYPE {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm ctx _ s@(Pi {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm ctx ty (Lam body loc) = do
|
|
let Pi {qty, arg, res, _} = ty
|
|
| _ => throw $ Expected "function type" ctx ty
|
|
case isErased qty of
|
|
Erased => do
|
|
-- replace with a fake name like "<erased x>"
|
|
-- a little trap for future me :3c
|
|
let name = baseStr body.name.val
|
|
dummy = F (unq $ UN "<erased \{name}>") 0 noLoc
|
|
eraseTerm ctx (sub1 res dummy) (sub1 body dummy)
|
|
Kept => do
|
|
let x = body.bname
|
|
U.Lam x <$> eraseTerm (extendTy x qty ctx) res.term body.term
|
|
|
|
eraseTerm ctx _ s@(Sig {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm ctx ty (Pair fst snd loc) = do
|
|
let Sig {fst = a, snd = b, _} = ty
|
|
| _ => throw $ Expected "pair type" ctx ty
|
|
let b = sub1 b (Ann fst a a.loc)
|
|
[|eraseTerm ctx a fst `Pair` eraseTerm ctx b snd|]
|
|
|
|
eraseTerm ctx _ s@(Enum {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm ctx _ (Tag tag loc) =
|
|
pure $ Tag tag
|
|
|
|
eraseTerm ctx ty s@(Eq {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm ctx ty (DLam body loc) = do
|
|
let Eq {ty = a, _} = ty
|
|
| _ => throw $ Expected "equality type" ctx ty
|
|
eraseTerm (extendDim body.bname ctx) a.term body.term
|
|
|
|
eraseTerm ctx _ s@(Nat {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm _ _ (Zero loc) =
|
|
pure Zero
|
|
|
|
eraseTerm ctx ty (Succ p loc) =
|
|
[|Succ $ eraseTerm ctx ty p|]
|
|
|
|
eraseTerm ctx ty s@(BOX {}) =
|
|
throw $ CompileTimeOnly ctx s
|
|
|
|
eraseTerm ctx ty (Box val loc) = do
|
|
let BOX {qty, ty = a, _} = ty
|
|
| _ => throw $ Expected "box type" ctx ty
|
|
case isErased qty of
|
|
Erased => pure ErasedBox -- lmao
|
|
Kept => eraseTerm ctx a val
|
|
|
|
eraseTerm ctx ty (E e) =
|
|
eraseElim ctx e
|
|
|
|
eraseTerm ctx ty (CloT (Sub term th)) =
|
|
eraseTerm ctx ty $ pushSubstsWith' id th term
|
|
|
|
eraseTerm ctx ty (DCloT (Sub term th)) =
|
|
eraseTerm ctx ty $ pushSubstsWith' th id term
|
|
|
|
eraseElim ctx e@(F x u loc) = do
|
|
Just def <- asks $ lookup x
|
|
| Nothing => throw $ NotInScope x
|
|
case isErased def.qty.qty of
|
|
Erased => throw $ CompileTimeOnly ctx $ E e
|
|
Kept => pure $ F x
|
|
|
|
eraseElim ctx e@(B i loc) = do
|
|
case ctx.erased !!! i of
|
|
Erased => throw $ CompileTimeOnly ctx $ E e
|
|
Kept => pure $ B i
|
|
|
|
eraseElim ctx (App fun arg loc) = ?eraseElim_rhs_2
|
|
|
|
eraseElim ctx (CasePair qty pair ret body loc) = ?eraseElim_rhs_3
|
|
|
|
eraseElim ctx (Fst pair loc) = ?eraseElim_rhs_4
|
|
|
|
eraseElim ctx (Snd pair loc) = ?eraseElim_rhs_5
|
|
|
|
eraseElim ctx (CaseEnum qty tag ret arms loc) = ?eraseElim_rhs_6
|
|
|
|
eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = ?eraseElim_rhs_7
|
|
|
|
eraseElim ctx (CaseBox qty box ret body loc) = ?eraseElim_rhs_8
|
|
|
|
eraseElim ctx (DApp fun arg loc) = ?eraseElim_rhs_9
|
|
|
|
eraseElim ctx (Ann tm ty loc) =
|
|
eraseTerm ctx ty tm
|
|
|
|
eraseElim ctx (Coe ty p q val loc) = ?eraseElim_rhs_11
|
|
|
|
eraseElim ctx (Comp ty p q val r zero one loc) = ?eraseElim_rhs_12
|
|
|
|
eraseElim ctx (TypeCase ty ret arms def loc) = ?eraseElim_rhs_13
|
|
|
|
eraseElim ctx (CloE (Sub term th)) =
|
|
eraseElim ctx $ pushSubstsWith' id th term
|
|
|
|
eraseElim ctx (DCloE (Sub term th)) =
|
|
eraseElim ctx $ pushSubstsWith' th id term
|