{-

Macros (autoDesc, AutoStructure, AutoEquivStr, autoUnivalentStr) for automatically generating structure definitions.

For example:

  autoDesc (λ (X : Type₀) → X → X × ℕ)   ↦   function+ var (var , constant ℕ)

We prefer to use the constant structure whenever possible, e.g., [autoDesc (λ (X : Type₀) → ℕ → ℕ)]
is [constant (ℕ → ℕ)] rather than [function (constant ℕ) (constant ℕ)].

Writing [auto* (λ X → ⋯)] doesn't seem to work, but [auto* (λ (X : Type ℓ) → ⋯)] does.

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Structures.Auto where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.List
open import Cubical.Data.Bool
open import Cubical.Data.Maybe
open import Cubical.Structures.Macro as Macro

import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

-- Magic number
private
  FUEL = 10000

-- Mark part of a structure definition to use transport-based structured equivalences
abstract
  Transp[_] :  {}  Type   Type 
  Transp[ A ] = A

-- Some reflection utilities
private
  tLevel = R.def (quote Level) []

  tType : R.Term  R.Term
  tType  = R.def (quote Type) [ varg  ]

  tTranspDesc : R.Term  R.Term  R.Term
  tTranspDesc  ℓ' = R.def (quote TranspDesc) ( v∷ ℓ' v∷ [])

  tDesc : R.Term  R.Term  R.Term  R.Term
  tDesc  ℓ₁ ℓ₁' = R.def (quote Desc) ( v∷ ℓ₁ v∷ ℓ₁' v∷ [])

  func : ( ℓ' : Level)  Type (ℓ-suc (ℓ-max  ℓ'))
  func  ℓ' = Type   Type ℓ'

  tStruct : R.Term  R.Term  R.Term
  tStruct  ℓ' = R.def (quote func) (varg   varg ℓ'  [])

-- We try to build a descriptor by unifying the provided structure with combinators we're aware of. We
-- redefine the structure combinators as the *Shape terms below so that we don't depend on the specific way
-- these are defined in other files (order of implicit arguments and so on); the syntactic analysis that goes
-- on here means that we would get mysterious errors if those changed.
private
  constantShape :  {ℓ'} ( : Level) (A : Type ℓ')  (Type   Type ℓ')
  constantShape _ A _ = A

  pointedShape : ( : Level)  Type   Type 
  pointedShape _ X = X

  productShape :  {ℓ₀ ℓ₁} ( : Level)
     (Type   Type ℓ₀)  (Type   Type ℓ₁)  Type   Type (ℓ-max ℓ₀ ℓ₁)
  productShape _ A₀ A₁ X = A₀ X × A₁ X

  functionShape :   {ℓ₀ ℓ₁} ( : Level)
     (Type   Type ℓ₀)  (Type   Type ℓ₁)  Type   Type (ℓ-max ℓ₀ ℓ₁)
  functionShape _ A₀ A₁ X = A₀ X  A₁ X

  maybeShape :  {ℓ₀} ( : Level)
     (Type   Type ℓ₀)  Type   Type ℓ₀
  maybeShape _ A₀ X = Maybe (A₀ X)

  transpShape :  {ℓ₀} ( : Level)
     (Type   Type ℓ₀)  Type   Type ℓ₀
  transpShape _ A₀ X = Transp[ A₀ X ]

private
  -- Build transport structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildTranspDesc :   R.Term  R.Term  R.Term  R.TC R.Term
  buildTranspDesc zero  ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n"  R.termErr t  [])
  buildTranspDesc (suc fuel)  ℓ' t =
    tryConstant t <|> tryPointed t <|> tryProduct t <|> tryFunction t <|> tryMaybe t <|>
    R.typeError (R.strErr "Can't automatically generate a transp structure for\n"  R.termErr t  [])
    where
    tryConstant : R.Term  R.TC R.Term
    tryConstant t =
      newMeta (tType ℓ') >>= λ A 
      R.unify t (R.def (quote constantShape) ( v∷ A v∷ [])) >>
      R.returnTC (R.con (quote TranspDesc.constant) (A v∷ []))

    tryPointed : R.Term  R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) ( v∷ [])) >>
      R.returnTC (R.con (quote TranspDesc.var) [])

    tryFunction : R.Term  R.TC R.Term
    tryFunction t =
      newMeta tLevel >>= λ ℓ₀ 
      newMeta tLevel >>= λ ℓ₁ 
      newMeta (tStruct  ℓ₀) >>= λ A₀ 
      newMeta (tStruct  ℓ₁) >>= λ A₁ 
      R.unify t (R.def (quote functionShape) ( v∷ A₀ v∷ A₁ v∷ [])) >>
      buildTranspDesc fuel  ℓ₀ A₀ >>= λ d₀ 
      buildTranspDesc fuel  ℓ₁ A₁ >>= λ d₁ 
      R.returnTC (R.con (quote TranspDesc.function) (d₀ v∷ d₁ v∷ []))

    tryProduct : R.Term  R.TC R.Term
    tryProduct t =
      newMeta tLevel >>= λ ℓ₀ 
      newMeta tLevel >>= λ ℓ₁ 
      newMeta (tStruct  ℓ₀) >>= λ A₀ 
      newMeta (tStruct  ℓ₁) >>= λ A₁ 
      R.unify t (R.def (quote productShape) ( v∷ A₀ v∷ A₁ v∷ [])) >>
      buildTranspDesc fuel  ℓ₀ A₀ >>= λ d₀ 
      buildTranspDesc fuel  ℓ₁ A₁ >>= λ d₁ 
      R.returnTC (R.con (quote TranspDesc._,_) (d₀ v∷ d₁ v∷ []))

    tryMaybe : R.Term  R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ 
      newMeta (tStruct  ℓ₀) >>= λ A₀ 
      R.unify t (R.def (quote maybeShape) ( v∷ A₀ v∷ [])) >>
      buildTranspDesc fuel  ℓ₀ A₀ >>= λ d₀ 
      R.returnTC (R.con (quote TranspDesc.maybe) (d₀ v∷ []))

  autoTranspDesc' : R.Term  R.Term  R.TC Unit
  autoTranspDesc' t hole =
    R.inferType hole >>= λ H 
    newMeta tLevel >>= λ  
    newMeta tLevel >>= λ ℓ' 
    R.unify (tTranspDesc  ℓ') H >>
    R.checkType t (tStruct  ℓ') >>
    buildTranspDesc FUEL  ℓ' t >>= R.unify hole

-- Build structure descriptor from a function [t : Type ℓ → Type ℓ']
buildDesc :   R.Term  R.Term  R.Term  R.TC R.Term
buildDesc zero  ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n"  R.termErr t  [])
buildDesc (suc fuel)  ℓ' t =
  tryConstant t <|> tryPointed t <|> tryProduct t <|> tryFunction t <|>
  tryMaybe t <|> tryTransp t <|>
  R.typeError (R.strErr "Can't automatically generate a structure for\n"  R.termErr t  [])
  where
  tryConstant : R.Term  R.TC R.Term
  tryConstant t =
    newMeta (tType ℓ') >>= λ A 
    R.unify t (R.def (quote constantShape) ( v∷ A v∷ [])) >>
    R.returnTC (R.con (quote Desc.constant) (A v∷ []))

  tryPointed : R.Term  R.TC R.Term
  tryPointed t =
    R.unify t (R.def (quote pointedShape) ( v∷ [])) >>
    R.returnTC (R.con (quote Desc.var) [])

  tryProduct : R.Term  R.TC R.Term
  tryProduct t =
    newMeta tLevel >>= λ ℓ₀ 
    newMeta tLevel >>= λ ℓ₁ 
    newMeta (tStruct  ℓ₀) >>= λ A₀ 
    newMeta (tStruct  ℓ₁) >>= λ A₁ 
    R.unify t (R.def (quote productShape) ( v∷ A₀ v∷ A₁ v∷ [])) >>
    buildDesc fuel  ℓ₀ A₀ >>= λ d₀ 
    buildDesc fuel  ℓ₁ A₁ >>= λ d₁ 
    R.returnTC (R.con (quote Desc._,_) (d₀ v∷ d₁ v∷ []))

  tryFunction : R.Term  R.TC R.Term
  tryFunction t =
    newMeta tLevel >>= λ ℓ₀ 
    newMeta tLevel >>= λ ℓ₁ 
    newMeta (tStruct  ℓ₀) >>= λ A₀ 
    newMeta (tStruct  ℓ₁) >>= λ A₁ 
    R.unify t (R.def (quote functionShape) ( v∷ A₀ v∷ A₁ v∷ [])) >>
    buildTranspDesc fuel  ℓ₀ A₀ >>= λ d₀ 
    buildDesc fuel  ℓ₁ A₁ >>= λ d₁ 
    R.returnTC (R.con (quote Desc.function+) (d₀ v∷ d₁ v∷ []))

  tryMaybe : R.Term  R.TC R.Term
  tryMaybe t =
    newMeta tLevel >>= λ ℓ₀ 
    newMeta (tStruct  ℓ₀) >>= λ A₀ 
    R.unify t (R.def (quote maybeShape) ( v∷ A₀ v∷ [])) >>
    buildDesc fuel  ℓ₀ A₀ >>= λ d₀ 
    R.returnTC (R.con (quote Desc.maybe) (d₀ v∷ []))

  tryTransp : R.Term  R.TC R.Term
  tryTransp t =
    newMeta (tStruct  ℓ') >>= λ A₀ 
    R.unify t (R.def (quote transpShape) ( v∷ A₀ v∷ [])) >>
    buildTranspDesc fuel  ℓ' A₀ >>= λ d₀ 
    R.returnTC (R.con (quote Desc.transpDesc) (d₀ v∷ []))

autoDesc' : R.Term  R.Term  R.TC Unit
autoDesc' t hole =
  R.inferType hole >>= λ H 
  newMeta tLevel >>= λ  
  newMeta tLevel >>= λ ℓ' 
  R.unify (tDesc  ℓ' R.unknown) H >>
  R.checkType t (tStruct  ℓ') >>
  buildDesc FUEL  ℓ' t >>= R.unify hole

macro
  -- (Type ℓ → Type ℓ₁) → TranspDesc ℓ
  autoTranspDesc : R.Term  R.Term  R.TC Unit
  autoTranspDesc = autoTranspDesc'

  -- (S : Type ℓ → Type ℓ₁) → EquivAction (AutoStructure S)
  autoEquivAction : R.Term  R.Term  R.TC Unit
  autoEquivAction t hole =
    newMeta (tTranspDesc R.unknown R.unknown) >>= λ d 
    R.unify hole (R.def (quote transpMacroAction) [ varg d ]) >>
    autoTranspDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → TransportStr (autoEquivAction S)
  autoTransportStr : R.Term  R.Term  R.TC Unit
  autoTransportStr t hole =
    newMeta (tTranspDesc R.unknown R.unknown) >>= λ d 
    R.unify hole (R.def (quote transpMacroTransportStr) [ varg d ]) >>
    autoTranspDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → Desc ℓ
  autoDesc : R.Term  R.Term  R.TC Unit
  autoDesc = autoDesc'

  -- (S : Type ℓ → Type ℓ₁) → (Type ℓ → Type ℓ₁)
  -- Removes Transp[_] annotations
  AutoStructure : R.Term  R.Term  R.TC Unit
  AutoStructure t hole =
    newMeta (tDesc R.unknown R.unknown R.unknown) >>= λ d 
    R.unify hole (R.def (quote MacroStructure) [ varg d ]) >>
    autoDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → StrEquiv (AutoStructure S) _
  AutoEquivStr : R.Term  R.Term  R.TC Unit
  AutoEquivStr t hole =
    newMeta (tDesc R.unknown R.unknown R.unknown) >>= λ d 
    R.unify hole (R.def (quote MacroEquivStr) [ varg d ]) >>
    autoDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → UnivalentStr (AutoStructure S) (AutoEquivStr S)
  autoUnivalentStr : R.Term  R.Term  R.TC Unit
  autoUnivalentStr t hole =
    newMeta (tDesc R.unknown R.unknown R.unknown) >>= λ d 
    R.unify hole (R.def (quote MacroUnivalentStr) [ varg d ]) >>
    autoDesc' t d