quox/lib/Quox/Whnf/Interface.idr

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 -> SQty -> 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) -> (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 : {d, n : Nat} -> {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 A‹0/𝑖› = A‹1/𝑖›), 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, _}) {d, n} =
    isJust $ lookupElim x u defs {d, n}
  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