Library MetaCoq.PCUIC.PCUICTypedAst

From Coq Require Import Morphisms.
From MetaCoq.Template Require Export utils Universes BasicAst Environment Reflect.
From MetaCoq.Template Require EnvironmentTyping.
From MetaCoq.PCUIC Require Export PCUICPrimitive.
From Equations Require Import Equations.
Require Vector Fin.

Inductive context (P : nat → Type) : nat → Type :=
| tnil : context P 0
| tcons {n} : P n → context P n → context P (S n).

Inductive context_decl (term : nat → Type) : nat → Type :=
| vass {n} (na : aname) (ty : term n) : context_decl term n
| vdef {n} (na : aname) (ty : term n) (body : term n) : context_decl term n.

Definition context_gen (term : nat → Type) :=
  context (context_decl term).

Definition shift n (f : nat → Type) :=
  fun i ⇒ f (n + i).

Variant FixCoFix :=
  | Fix | CoFix.


Variant global_reference :=
  | ConstRef (kn : kername)
  | IndRef (ind : inductive)
  | ConstructRef (ind : inductive) (k : nat).

Definition global_env (term : nat → Type) := list (kername × term 0).

Fixpoint lookup_env {term} (Σ : global_env term) (kn : kername) : option (term 0) :=
  match Σ with
  | nil ⇒ None
  | d :: tl ⇒
    if eq_kername kn d.1 then Some d.2
    else lookup_env tl kn
  end.

Definition declared_constant {term} (Σ : global_env term) (id : kername) : Type :=
  ∑ decl, lookup_env Σ id = Some decl.

Inductive term {k : nat} : Type :=
| tRel (f : Fin.t k)
| tVar (i : ident)
| tEvar (n : nat) (l : list term)
| tSort (u : Universe.t)
| tProd (na : aname) (A : term) (B : @term Σ (S k))
| tLambda (na : aname) (A : term) (B : @term Σ (S k))
| tLetIn (na : aname) (b B : term) (t : @term Σ (S k))
| tApp (u v : term)
| tConst (kn : kername) (ui : Instance.t)
  (declared_constant Σ kn)

| tConstruct (ind : inductive) (n : nat) (ui : Instance.t)
| tCase {plen} (indn : case_info) (pparams : list term) (puinst : Instance.t)
  (pcontext : context_gen (shift k (@term Σ)) plen)
  (c : term)
  (brs : list (∑ brlen (ctx : context_gen (@term Σ) brlen), @term Σ (brlen + k)))
| tProj (p : projection) (c : term)
| tFix (e : FixCoFix) {n} (mfix : Vector.t (def term) n) (idx : Fin.t n)

| tPrim (prim : prim_val term).

with branch {n : nat} := Type :=
| vass (na : aname) (t : term k)

with global_env : Type :=
.