Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More unified judgment type and All_local_env #1007

Merged
merged 6 commits into from
Dec 19, 2023
Merged

More unified judgment type and All_local_env #1007

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8a07c40
More unified "judgment" type
yannl35133 Oct 27, 2023
c9f169b
More unified All_local_env, cleaned up {PCUIC,}Typing
yannl35133 Nov 7, 2023
9b74e81
Shared app_context, integrated Σ in ctx_inst
yannl35133 Nov 8, 2023
e4a179c
Change typing rules for lambda prod and letin
yannl35133 Nov 15, 2023
3a488f5
Rename LevelAlg -> Universe.t -> Sort.t, equality takes conv_pb
yannl35133 Dec 15, 2023
078344e
Fix translations
yannl35133 Dec 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 62 additions & 15 deletions common/theories/BasicAst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,20 +213,17 @@ Proof.
eapply map_def_spec; eauto.
Qed.

Variant typ_or_sort_ {term} := Typ (T : term) | Sort.
Arguments typ_or_sort_ : clear implicits.

Definition typ_or_sort_map {T T'} (f: T -> T') t :=
match t with
| Typ T => Typ (f T)
| Sort => Sort
end.

Definition typ_or_sort_default {T A} (f: T -> A) t d :=
match t with
| Typ T => f T
| Sort => d
end.
Record judgment_ {universe Term} := Judge {
j_term : option Term;
j_typ : Term;
j_univ : option universe;
(* j_rel : option relevance; *)
}.
Arguments judgment_ : clear implicits.
Arguments Judge {universe Term} _ _ _.

Definition judgment_map {univ T A} (f: T -> A) (j : judgment_ univ T) :=
Judge (option_map f (j_term j)) (f (j_typ j)) (j_univ j) (* (j_rel j) *).

Section Contexts.
Context {term : Type}.
Expand All @@ -242,6 +239,18 @@ End Contexts.

Arguments context_decl : clear implicits.

Notation Typ typ := (Judge None typ None).
Notation TermTyp tm ty := (Judge (Some tm) ty None).
Notation TermoptTyp tm typ := (Judge tm typ None).
Notation TypUniv ty u := (Judge None ty (Some u)).
Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u)).

Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)).
Notation j_vass_s na ty s := (TypUniv ty s (* na.(binder_relevance) *)).
Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)).
Notation j_decl d := (TermoptTyp (decl_body d) (decl_type d) (* (decl_name d).(binder_relevance) *)).
Notation j_decl_s d s := (Judge (decl_body d) (decl_type d) s (* (decl_name d).(binder_relevance) *)).

Definition map_decl {term term'} (f : term -> term') (d : context_decl term) : context_decl term' :=
{| decl_name := d.(decl_name);
decl_body := option_map f d.(decl_body);
Expand Down Expand Up @@ -308,8 +317,46 @@ Definition snoc {A} (Γ : list A) (d : A) := d :: Γ.

Notation " Γ ,, d " := (snoc Γ d) (at level 20, d at next level).

Definition app_context {A} (Γ Γ': list A) := Γ' ++ Γ.

Notation "Γ ,,, Γ'" := (app_context Γ Γ') (at level 25, Γ' at next level, left associativity).

Lemma app_context_nil_l {T} Γ : [] ,,, Γ = Γ :> list T.
Proof.
unfold app_context. rewrite app_nil_r. reflexivity.
Qed.

Lemma app_context_assoc {T} Γ Γ' Γ'' : Γ ,,, (Γ' ,,, Γ'') = Γ ,,, Γ' ,,, Γ'' :> list T.
Proof. unfold app_context; now rewrite app_assoc. Qed.

Lemma app_context_cons {T} Γ Γ' A : Γ ,,, (Γ' ,, A) = (Γ ,,, Γ') ,, A :> list T.
Proof. exact (app_context_assoc _ _ [A]). Qed.

Lemma app_context_push {T} Γ Δ Δ' d : (Γ ,,, Δ ,,, Δ') ,, d = (Γ ,,, Δ ,,, (Δ' ,, d)) :> list T.
Proof using Type.
reflexivity.
Qed.

Lemma snoc_app_context {T Γ Δ d} : (Γ ,,, (d :: Δ)) = (Γ ,,, Δ) ,,, [d] :> list T.
Proof using Type.
reflexivity.
Qed.

Lemma app_context_length {T} (Γ Γ' : list T) : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|.
Proof. unfold app_context. now rewrite app_length. Qed.
#[global] Hint Rewrite @app_context_length : len.

Lemma nth_error_app_context_ge {T} v Γ Γ' :
#|Γ'| <= v -> nth_error (Γ ,,, Γ') v = nth_error Γ (v - #|Γ'|) :> option T.
Proof. apply nth_error_app_ge. Qed.

Lemma nth_error_app_context_lt {T} v Γ Γ' :
v < #|Γ'| -> nth_error (Γ ,,, Γ') v = nth_error Γ' v :> option T.
Proof. apply nth_error_app_lt. Qed.


Definition ondecl {A} (P : A -> Type) (d : context_decl A) :=
P d.(decl_type) × option_default P d.(decl_body) unit.
option_default P d.(decl_body) unit × P d.(decl_type).

Notation onctx P := (All (ondecl P)).

Expand Down
42 changes: 6 additions & 36 deletions common/theories/Environment.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Module Type Term.
Parameter Inline term : Type.

Parameter Inline tRel : nat -> term.
Parameter Inline tSort : Universe.t -> term.
Parameter Inline tSort : Sort.t -> term.
Parameter Inline tProd : aname -> term -> term -> term.
Parameter Inline tLambda : aname -> term -> term -> term.
Parameter Inline tLetIn : aname -> term -> term -> term -> term.
Expand Down Expand Up @@ -129,7 +129,7 @@ Module Environment (T : Term).
Import T.
#[global] Existing Instance subst_instance_constr.

Definition typ_or_sort := typ_or_sort_ term.
Definition judgment := judgment_ Sort.t term.

(** ** Declarations *)
Notation context_decl := (context_decl term).
Expand Down Expand Up @@ -344,7 +344,7 @@ Module Environment (T : Term).
Record one_inductive_body := {
ind_name : ident;
ind_indices : context; (* Indices of the inductive types, under params *)
ind_sort : Universe.t; (* Sort of the inductive. *)
ind_sort : Sort.t; (* Sort of the inductive. *)
ind_type : term; (* Closed arity = forall mind_params, ind_indices, tSort ind_sort *)
ind_kelim : allowed_eliminations; (* Allowed eliminations *)
ind_ctors : list constructor_body;
Expand Down Expand Up @@ -856,10 +856,10 @@ Module Environment (T : Term).
Definition primitive_invariants (p : prim_tag) (cdecl : constant_body) :=
match p with
| primInt | primFloat =>
[/\ cdecl.(cst_type) = tSort Universe.type0, cdecl.(cst_body) = None &
[/\ cdecl.(cst_type) = tSort Sort.type0, cdecl.(cst_body) = None &
cdecl.(cst_universes) = Monomorphic_ctx]
| primArray =>
let s := Universe.make (Level.lvar 0) in
let s := sType (Universe.make' (Level.lvar 0)) in
[/\ cdecl.(cst_type) = tImpl (tSort s) (tSort s), cdecl.(cst_body) = None &
cdecl.(cst_universes) = Polymorphic_ctx array_uctx]
end.
Expand All @@ -882,12 +882,6 @@ Module Environment (T : Term).

Definition program : Type := global_env * term.

(* TODO MOVE AstUtils factorisation *)

Definition app_context (Γ Γ' : context) : context := Γ' ++ Γ.
Notation "Γ ,,, Γ'" :=
(app_context Γ Γ') (at level 25, Γ' at next level, left associativity).

(** Make a lambda/let-in string of abstractions from a context [Γ], ending with term [t]. *)

Definition mkLambda_or_LetIn d t :=
Expand Down Expand Up @@ -1008,30 +1002,6 @@ Module Environment (T : Term).
Proof. unfold arities_context. now rewrite rev_map_length. Qed.
#[global] Hint Rewrite arities_context_length : len.

Lemma app_context_nil_l Γ : [] ,,, Γ = Γ.
Proof.
unfold app_context. rewrite app_nil_r. reflexivity.
Qed.

Lemma app_context_assoc Γ Γ' Γ'' : Γ ,,, (Γ' ,,, Γ'') = Γ ,,, Γ' ,,, Γ''.
Proof. unfold app_context; now rewrite app_assoc. Qed.

Lemma app_context_cons Γ Γ' A : Γ ,,, (Γ' ,, A) = (Γ ,,, Γ') ,, A.
Proof. exact (app_context_assoc _ _ [A]). Qed.

Lemma app_context_length Γ Γ' : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|.
Proof. unfold app_context. now rewrite app_length. Qed.
#[global] Hint Rewrite app_context_length : len.

Lemma nth_error_app_context_ge v Γ Γ' :
#|Γ'| <= v -> nth_error (Γ ,,, Γ') v = nth_error Γ (v - #|Γ'|).
Proof. apply nth_error_app_ge. Qed.

Lemma nth_error_app_context_lt v Γ Γ' :
v < #|Γ'| -> nth_error (Γ ,,, Γ') v = nth_error Γ' v.
Proof. apply nth_error_app_lt. Qed.


Definition map_mutual_inductive_body f m :=
match m with
| Build_mutual_inductive_body finite ind_npars ind_pars ind_bodies ind_universes ind_variance =>
Expand Down Expand Up @@ -1269,7 +1239,7 @@ End EnvironmentDecideReflectInstances.
Module Type TermUtils (T: Term) (E: EnvironmentSig T).
Import T E.

Parameter Inline destArity : context -> term -> option (context × Universe.t).
Parameter Inline destArity : context -> term -> option (context × Sort.t).
Parameter Inline inds : kername -> Instance.t -> list one_inductive_body -> list term.

End TermUtils.
Loading
Loading