quox/lib/Quox/Whnf/Interface.idr
2023-11-03 18:05:54 +01:00

237 lines
7.8 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 -> 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 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 -> SQty -> Pred (tm d n)
IsRedex defs q = So . isRedex defs q
NotRedex defs q = No . isRedex defs q
public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
CanWhnf tm isRedex => (d, n : Nat) ->
(defs : Definitions) -> SQty -> Type
NonRedex tm d n defs q = Subset (tm d n) (NotRedex defs q)
public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs q t) => NonRedex tm d n defs 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 `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 : SQty -> (ty, val : Term {}) -> Bool
canPushCoe sg (TYPE {}) _ = 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 (Zero {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = 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. 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
public export
isRedexE : RedexTest Elim
isRedexE defs sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
isRedexE _ sg (B {}) = False
isRedexE defs sg (App {fun, _}) =
isRedexE defs sg fun || isLamHead fun
isRedexE defs sg (CasePair {pair, _}) =
isRedexE defs sg pair || isPairHead pair || isYes (sg `decEq` SZero)
isRedexE defs sg (Fst pair _) =
isRedexE defs sg pair || isPairHead pair
isRedexE defs sg (Snd pair _) =
isRedexE defs sg pair || isPairHead pair
isRedexE defs sg (CaseEnum {tag, _}) =
isRedexE defs sg tag || isTagHead tag
isRedexE defs sg (CaseNat {nat, _}) =
isRedexE defs sg nat || isNatHead nat
isRedexE defs sg (CaseBox {box, _}) =
isRedexE defs sg box || isBoxHead box
isRedexE defs sg (DApp {fun, arg, _}) =
isRedexE defs sg fun || isDLamHead fun || isK arg
isRedexE defs sg (Ann {tm, ty, _}) =
isE tm || isRedexT defs sg tm || isRedexT defs SZero ty
isRedexE defs sg (Coe {ty = S _ (N _), _}) = True
isRedexE defs sg (Coe {ty = S _ (Y ty), p, q, val, _}) =
isRedexT defs SZero ty || canPushCoe sg ty val || isYes (p `decEqv` q)
isRedexE defs sg (Comp {ty, p, q, r, _}) =
isYes (p `decEqv` q) || isK r
isRedexE defs sg (TypeCase {ty, ret, _}) =
isRedexE defs sg ty || isRedexT defs 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
public export
isRedexT : RedexTest Term
isRedexT _ _ (CloT {}) = True
isRedexT _ _ (DCloT {}) = True
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
isRedexT _ _ _ = False