quox/lib/Quox/Whnf/Interface.idr

235 lines
7.5 KiB
Idris
Raw Normal View History

2023-08-24 12:42:26 -04:00
module Quox.Whnf.Interface
import public Quox.No
import public Quox.Syntax
import public Quox.Definition
import public Quox.Typing.Context
import public Quox.Typing.Error
import public Data.Maybe
import public Control.Eff
%default total
public export
Whnf : List (Type -> Type)
Whnf = [NameGen, Except Error]
public export
0 RedexTest : TermLike -> Type
RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
public export
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
whnf : {d, n : Nat} -> (defs : Definitions) ->
(ctx : WhnfContext d n) ->
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
-- having isRedex be part of the class header, and needing to be explicitly
-- quantified on every use since idris can't infer its type, is a little ugly.
-- but none of the alternatives i've thought of so far work. e.g. in some
-- cases idris can't tell that `isRedex` and `isRedexT` are the same thing
public export %inline
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
(defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n)
whnf0 defs ctx t = fst <$> whnf defs ctx t
public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> Pred (tm d n)
IsRedex defs = So . isRedex defs
NotRedex defs = No . isRedex defs
public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
CanWhnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
nred t = Element t nr
||| an expression like `(λ x ⇒ s) ∷ π.(x : A) → B`
public export %inline
isLamHead : Elim {} -> Bool
isLamHead (Ann (Lam {}) (Pi {}) _) = True
isLamHead (Coe {}) = True
isLamHead _ = False
||| an expression like `(δ 𝑖 ⇒ s) ∷ Eq (𝑖 ⇒ A) s t`
public export %inline
isDLamHead : Elim {} -> Bool
isDLamHead (Ann (DLam {}) (Eq {}) _) = True
isDLamHead (Coe {}) = True
isDLamHead _ = False
||| an expression like `(s, t) ∷ (x : A) × B`
public export %inline
isPairHead : Elim {} -> Bool
isPairHead (Ann (Pair {}) (Sig {}) _) = True
isPairHead (Coe {}) = True
isPairHead _ = False
||| an expression like `'a ∷ {a, b, c}`
public export %inline
isTagHead : Elim {} -> Bool
isTagHead (Ann (Tag {}) (Enum {}) _) = True
isTagHead (Coe {}) = True
isTagHead _ = False
||| an expression like `0 ∷ ` or `suc n ∷ `
public export %inline
isNatHead : Elim {} -> Bool
isNatHead (Ann (Zero {}) (Nat {}) _) = True
isNatHead (Ann (Succ {}) (Nat {}) _) = True
isNatHead (Coe {}) = True
isNatHead _ = False
||| an expression like `[s] ∷ [π. A]`
public export %inline
isBoxHead : Elim {} -> Bool
isBoxHead (Ann (Box {}) (BOX {}) _) = True
isBoxHead (Coe {}) = True
isBoxHead _ = False
||| an elimination in a term context
public export %inline
isE : Term {} -> Bool
isE (E {}) = True
isE _ = False
||| an expression like `s ∷ A`
public export %inline
isAnn : Elim {} -> Bool
isAnn (Ann {}) = True
isAnn _ = False
||| a syntactic type
public export %inline
isTyCon : Term {} -> Bool
isTyCon (TYPE {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (Nat {}) = True
isTyCon (Zero {}) = False
isTyCon (Succ {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
||| a syntactic type, or a neutral
public export %inline
isTyConE : Term {} -> Bool
isTyConE s = isTyCon s || isE s
||| a syntactic type with an annotation `★ᵢ`
public export %inline
isAnnTyCon : Elim {} -> Bool
isAnnTyCon (Ann ty (TYPE {}) _) = isTyCon ty
isAnnTyCon _ = False
||| 0 or 1
public export %inline
isK : Dim d -> Bool
isK (K {}) = True
isK _ = False
||| if `ty` is a type constructor, and `val` is a value of that type where a
||| coercion can be reduced. which is the case if any of:
||| - `ty` is an atomic type
||| - `ty` has η
||| - `val` is a constructor form
public export %inline
canPushCoe : (ty, val : Term {}) -> Bool
canPushCoe (TYPE {}) _ = True
canPushCoe (Pi {}) _ = True
canPushCoe (Lam {}) _ = False
canPushCoe (Sig {}) (Pair {}) = True
canPushCoe (Sig {}) _ = False
canPushCoe (Pair {}) _ = False
canPushCoe (Enum {}) _ = True
canPushCoe (Tag {}) _ = False
canPushCoe (Eq {}) _ = True
canPushCoe (DLam {}) _ = False
canPushCoe (Nat {}) _ = True
canPushCoe (Zero {}) _ = False
canPushCoe (Succ {}) _ = False
canPushCoe (BOX {}) _ = True
canPushCoe (Box {}) _ = False
canPushCoe (E {}) _ = False
canPushCoe (CloT {}) _ = False
canPushCoe (DCloT {}) _ = False
2023-08-24 12:42:26 -04:00
mutual
||| a reducible elimination
|||
||| 1. a free variable, if its definition is known
||| 2. an elimination whose head is reducible
||| 3. an "active" elimination:
||| an application whose head is an annotated lambda,
||| a case expression whose head is an annotated constructor form, etc
||| 4. a redundant annotation, or one whose term or type is reducible
||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
||| a. `A` is reducible or a type constructor, or
||| b. `𝑖` is not mentioned in `A`
||| ([fixme] should be A0/𝑖 = A1/𝑖), or
||| c. `p = q`
||| 6. a composition `comp A @p @q s @r {⋯}`
||| where `p = q`, `r = 0`, or `r = 1`
||| 7. a closure
2023-08-24 12:42:26 -04:00
public export
isRedexE : RedexTest Elim
isRedexE defs (F {x, _}) {d, n} =
isJust $ lookupElim x defs {d, n}
isRedexE _ (B {}) = False
isRedexE defs (App {fun, _}) =
isRedexE defs fun || isLamHead fun
isRedexE defs (CasePair {pair, _}) =
isRedexE defs pair || isPairHead pair
isRedexE defs (CaseEnum {tag, _}) =
isRedexE defs tag || isTagHead tag
isRedexE defs (CaseNat {nat, _}) =
isRedexE defs nat || isNatHead nat
isRedexE defs (CaseBox {box, _}) =
isRedexE defs box || isBoxHead box
isRedexE defs (DApp {fun, arg, _}) =
isRedexE defs fun || isDLamHead fun || isK arg
isRedexE defs (Ann {tm, ty, _}) =
isE tm || isRedexT defs tm || isRedexT defs ty
isRedexE defs (Coe {ty = S _ (N _), _}) = True
isRedexE defs (Coe {ty = S _ (Y ty), p, q, val, _}) =
isRedexT defs ty || canPushCoe ty val || isYes (p `decEqv` q)
isRedexE defs (Comp {ty, r, p, q, _}) =
isYes (p `decEqv` q) || isK r
2023-08-24 12:42:26 -04:00
isRedexE defs (TypeCase {ty, ret, _}) =
isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
isRedexE _ (CloE {}) = True
isRedexE _ (DCloE {}) = True
||| a reducible term
|||
||| 1. a reducible elimination, as `isRedexE`
||| 2. an annotated elimination
||| (the annotation is redundant in a checkable context)
||| 3. a closure
2023-08-24 12:42:26 -04:00
public export
isRedexT : RedexTest Term
isRedexT _ (CloT {}) = True
isRedexT _ (DCloT {}) = True
isRedexT defs (E {e, _}) = isAnn e || isRedexE defs e
isRedexT _ _ = False