Library MetaRocq.PCUIC.PCUICTypedAst

From Stdlib Require Import Morphisms.
From MetaRocq.Common Require Export utils Universes BasicAst Environment Reflect.
From MetaRocq.Common Require EnvironmentTyping.
From MetaRocq.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 : sort)
| 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 :=
.