Merge pull request #1007 from yannl35133/rejudgment

More unified judgment type and All_local_env

common/theories/BasicAst.v

@@ -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}.
@@ -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);
@@ -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)).
 

common/theories/Environment.v

@@ -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.
@@ -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).
@@ -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;
@@ -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.
@@ -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 :=
@@ -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 =>
@@ -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.