quox/lib/Quox/Whnf/Interface.idr

262 lines
9 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 = [Except Error, NameGen]
public export
0 RedexTest : TermLike -> Type
RedexTest tm =
{0 d, n : Nat} -> Definitions -> WhnfContext d n -> SQty -> tm d n -> Bool
public export
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
-- 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 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
whnf0 defs ctx q t = fst <$> whnf defs ctx q t
public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> WhnfContext d n -> SQty -> Pred (tm d n)
IsRedex defs ctx q = So . isRedex defs ctx q
NotRedex defs ctx q = No . isRedex defs ctx q
public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
CanWhnf tm isRedex => (d, n : Nat) ->
Definitions -> WhnfContext d n -> SQty -> Type
NonRedex tm d n defs ctx q = Subset (tm d n) (NotRedex defs ctx q)
public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs ctx q t) =>
NonRedex tm d n defs ctx q
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 `𝑘` for a natural constant 𝑘, or `suc n ∷ `
public export %inline
isNatHead : Elim {} -> Bool
isNatHead (Ann (Nat {}) (NAT {}) _) = True
isNatHead (Ann (Succ {}) (NAT {}) _) = True
isNatHead (Coe {}) = True
isNatHead _ = False
||| a natural constant, with or without an annotation
public export %inline
isNatConst : Term d n -> Bool
isNatConst (Nat {}) = True
isNatConst (E (Ann (Nat {}) _ _)) = True
isNatConst _ = 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 (IOState {}) = 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 (Nat {}) = False
isTyCon (Succ {}) = False
isTyCon (STRING {}) = True
isTyCon (Str {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (Let {}) = 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
||| true if `ty` is a type constructor, and `val` is a value of that type where
||| a coercion can be reduced
|||
||| 1. `ty` is an atomic type
||| 2. `ty` has an η law that is usable in this context
||| (e.g. η for pairs only exists when σ=0, not when σ=1)
||| 3. `val` is a constructor form
public export %inline
canPushCoe : SQty -> (ty, val : Term {}) -> Bool
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (IOState {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (NAT {}) _ = True
canPushCoe sg (Nat {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (STRING {}) _ = True
canPushCoe sg (Str {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (Let {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
mutual
||| a reducible elimination
|||
||| 1. a free variable, if its definition is known
||| 2. a bound variable pointing to a `let`
||| 3. an elimination whose head is reducible
||| 4. an "active" elimination:
||| an application whose head is an annotated lambda,
||| a case expression whose head is an annotated constructor form, etc
||| 5. a redundant annotation, or one whose term or type is reducible
||| 6. 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`
||| 7. a composition `comp A @p @q s @r {⋯}`
||| where `p = q`, `r = 0`, or `r = 1`
||| 8. a closure
public export
isRedexE : RedexTest Elim
isRedexE defs ctx sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
isRedexE _ ctx sg (B {i, _}) = isJust (ctx.tctx !! i).term
isRedexE defs ctx sg (App {fun, _}) =
isRedexE defs ctx sg fun || isLamHead fun
isRedexE defs ctx sg (CasePair {pair, _}) =
isRedexE defs ctx sg pair || isPairHead pair || isYes (sg `decEq` SZero)
isRedexE defs ctx sg (Fst pair _) =
isRedexE defs ctx sg pair || isPairHead pair
isRedexE defs ctx sg (Snd pair _) =
isRedexE defs ctx sg pair || isPairHead pair
isRedexE defs ctx sg (CaseEnum {tag, _}) =
isRedexE defs ctx sg tag || isTagHead tag
isRedexE defs ctx sg (CaseNat {nat, _}) =
isRedexE defs ctx sg nat || isNatHead nat
isRedexE defs ctx sg (CaseBox {box, _}) =
isRedexE defs ctx sg box || isBoxHead box
isRedexE defs ctx sg (DApp {fun, arg, _}) =
isRedexE defs ctx sg fun || isDLamHead fun || isK arg
isRedexE defs ctx sg (Ann {tm, ty, _}) =
isE tm || isRedexT defs ctx sg tm || isRedexT defs ctx SZero ty
isRedexE defs ctx sg (Coe {ty = S _ (N _), _}) = True
isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, q, val, _}) =
isRedexT defs (extendDim i ctx) SZero ty ||
canPushCoe sg ty val || isYes (p `decEqv` q)
isRedexE defs ctx sg (Comp {ty, p, q, r, _}) =
isYes (p `decEqv` q) || isK r
isRedexE defs ctx sg (TypeCase {ty, ret, _}) =
isRedexE defs ctx sg ty || isRedexT defs ctx sg 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
||| 4. `succ` applied to a natural constant
||| 5. a `let` expression
public export
isRedexT : RedexTest Term
isRedexT _ _ _ (CloT {}) = True
isRedexT _ _ _ (DCloT {}) = True
isRedexT _ _ _ (Let {}) = True
isRedexT defs ctx sg (E {e, _}) = isAnn e || isRedexE defs ctx sg e
isRedexT _ _ _ (Succ p {}) = isNatConst p
isRedexT _ _ _ _ = False