267 lines
9.1 KiB
Idris
267 lines
9.1 KiB
Idris
module Quox.Whnf.Interface
|
||
|
||
import public Quox.No
|
||
import public Quox.Log
|
||
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, Log]
|
||
|
||
|
||
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, whnfNoLog :
|
||
(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, whnfNoLog0 :
|
||
{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
|
||
whnfNoLog0 defs ctx q t = fst <$> whnfNoLog 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 A‹0/𝑖› = A‹1/𝑖›), 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
|