{-# 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
private
FUEL = 10000
abstract
Transp[_] : ∀ {ℓ} → Type ℓ → Type ℓ
Transp[ A ] = A
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 ℓ' ∷ [])
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
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
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
autoTranspDesc : R.Term → R.Term → R.TC Unit
autoTranspDesc = autoTranspDesc'
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
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
autoDesc : R.Term → R.Term → R.TC Unit
autoDesc = autoDesc'
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
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
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