08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
123 lines
4.7 KiB
Text
123 lines
4.7 KiB
Text
section
|
||
variable (G : Type 1) (T : Type 1) (Tm : Type 1)
|
||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||
(getCtx : T → G) (getTy : Tm → T)
|
||
inductive CtxSyntaxLayer where
|
||
| emp : CtxSyntaxLayer
|
||
| snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
|
||
end
|
||
section
|
||
variable (G : Type 1) (T : Type 1) (Tm : Type 1)
|
||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||
(getCtx : T → G) (getTy : Tm → T)
|
||
(GAlgebra : CtxSyntaxLayer G T EG getCtx → G)
|
||
|
||
inductive TySyntaxLayer where
|
||
| top : {Γ : G} → TySyntaxLayer
|
||
| bot : {Γ : G} → TySyntaxLayer
|
||
| nat : {Γ : G} → TySyntaxLayer
|
||
| arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
|
||
|
||
def getCtxStep : TySyntaxLayer G T EG getCtx → G
|
||
| TySyntaxLayer.top (Γ := Γ) .. => Γ
|
||
| TySyntaxLayer.bot (Γ := Γ) .. => Γ
|
||
| TySyntaxLayer.nat (Γ := Γ) .. => Γ
|
||
| TySyntaxLayer.arrow (Γ := Γ) .. => Γ
|
||
end
|
||
section
|
||
variable (G : Type 1) (T : Type 1) (Tm : Type 1)
|
||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||
(EGrfl : ∀ {Γ}, EG Γ Γ)
|
||
(getCtx : T → G) (getTy : Tm → T)
|
||
(GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)
|
||
|
||
inductive TmSyntaxLayer where
|
||
| tt : {Γ : G} → TmSyntaxLayer
|
||
| zero : {Γ : G} → TmSyntaxLayer
|
||
| succ : {Γ : G} → TmSyntaxLayer
|
||
| app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
|
||
→ (f x : Tm)
|
||
→ ET (getTy f) (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx))
|
||
→ ET (getTy x) A
|
||
→ TmSyntaxLayer
|
||
-- set options for debugging "(kernel) declaration has metavariables" errors
|
||
--set_option trace.Elab.definition true
|
||
--set_option pp.explicit true
|
||
def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
|
||
| TmSyntaxLayer.tt (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.top (Γ:=Γ))
|
||
| TmSyntaxLayer.zero (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.nat (Γ:=Γ))
|
||
| TmSyntaxLayer.succ (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) EGrfl EGrfl)
|
||
| TmSyntaxLayer.app (B:=B) .. => B
|
||
end
|
||
|
||
structure SyntaxModel where
|
||
Ctx : Type 1
|
||
Ty : Type 1
|
||
Tm : Type 1
|
||
EC : Ctx → Ctx → Type
|
||
ETy : Ty → Ty → Type
|
||
ETm : Tm → Tm → Type
|
||
getCtx : Ty → Ctx
|
||
getTy : Tm → Ty
|
||
interpCStep : CtxSyntaxLayer Ctx Ty EC getCtx → Ctx
|
||
interpTyStep : TySyntaxLayer Ctx Ty EC getCtx → Ty
|
||
interpTmStep : TmSyntaxLayer Ctx Ty Tm EC ETy getCtx getTy interpTyStep → Tm
|
||
|
||
namespace SetModel
|
||
def Ctx := Type
|
||
structure Ty where
|
||
ctx : Ctx
|
||
ty : ctx → Type
|
||
structure Tm where
|
||
ty : Ty
|
||
tm : ∀ {Γ}, ty.ty Γ
|
||
|
||
def ECtx : Ctx → Ctx → Type := (PLift $ · = ·)
|
||
def ETy : Ty → Ty → Type := (PLift $ · = ·)
|
||
def ETm : Tm → Tm → Type := (PLift $ · = ·)
|
||
|
||
def interpCStep : CtxSyntaxLayer Ctx Ty ECtx Ty.ctx → Ctx
|
||
| CtxSyntaxLayer.emp => Unit
|
||
| CtxSyntaxLayer.snoc _ T (PLift.up rfl) => Σ γ : _, T.ty γ
|
||
|
||
def Ty.inj Γ T := Ty.mk Γ (λ _ => T)
|
||
def Ty.Unit {Γ} := Ty.inj Γ _root_.Unit
|
||
def Ty.Empty {Γ} := Ty.inj Γ _root_.Empty
|
||
def Ty.Nat {Γ} := Ty.inj Γ _root_.Nat
|
||
|
||
def Tm.inj Γ {T} (t : T) := Tm.mk (Ty.inj Γ T) t
|
||
|
||
def interpTyStep : TySyntaxLayer Ctx Ty ECtx Ty.ctx → Ty
|
||
| TySyntaxLayer.top (Γ:=Γ) => Ty.Unit (Γ:=Γ)
|
||
| TySyntaxLayer.bot (Γ:=Γ) => Ty.Empty (Γ:=Γ)
|
||
| TySyntaxLayer.nat (Γ:=Γ) => Ty.Nat (Γ:=Γ)
|
||
| TySyntaxLayer.arrow (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) => Ty.mk Γ (λ γ => A.ty (cast Actx γ) → B.ty (cast Bctx γ))
|
||
|
||
def interpTmStep : TmSyntaxLayer Ctx Ty Tm ECtx ETy Ty.ctx Tm.ty interpTyStep → Tm
|
||
| TmSyntaxLayer.tt (Γ:=Γ) => Tm.inj Γ Unit.unit
|
||
| TmSyntaxLayer.zero (Γ:=Γ) => Tm.inj Γ (0 : Nat)
|
||
| TmSyntaxLayer.succ (Γ:=Γ) => Tm.inj Γ Nat.succ
|
||
| TmSyntaxLayer.app (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) (Tm.mk fty ftm) (Tm.mk (Ty.mk xctx xty) xtm) (PLift.up fTy) (PLift.up xTy)
|
||
=> { ty := B
|
||
, tm := fun {γ} =>
|
||
(by
|
||
simp at fTy xTy; subst fTy xTy; simp at Actx Bctx; subst Actx Bctx
|
||
exact (ftm xtm)
|
||
)
|
||
}
|
||
|
||
def Model : SyntaxModel :=
|
||
{
|
||
Ctx := Ctx
|
||
, Ty := Ty
|
||
, Tm := Tm
|
||
, EC := ECtx
|
||
, ETy := ETy
|
||
, ETm := ETm
|
||
, getCtx := Ty.ctx
|
||
, getTy := Tm.ty
|
||
, interpCStep := interpCStep
|
||
, interpTyStep := interpTyStep
|
||
, interpTmStep := interpTmStep
|
||
}
|
||
end SetModel
|