sorts_family in checker and fix .v files as well w.r.t. change of sort

src/template_coq.ml4

@@ -21,6 +21,7 @@ struct
   type quoted_ident = char list
   type quoted_name = name
   type quoted_sort = sort
+  type quoted_sort_family = sort_family
   type quoted_cast_kind = cast_kind
   type quoted_kernel_name = char list
   type quoted_inductive = inductive
@@ -50,6 +51,12 @@ struct
     | Prop Null -> Coq_sProp
     | Prop Pos -> Coq_sSet
     | Type i -> Coq_sType (pos_of_universe i)
+
+  let quote_sort_family s =
+    match s with
+    | Sorts.InProp -> Ast0.InProp
+    | Sorts.InSet -> Ast0.InSet
+    | Sorts.InType -> Ast0.InType
 
   let quote_cast_kind = function
     | DEFAULTcast -> Cast
@@ -115,11 +122,12 @@ struct
   let mkMutualInductive kn p r =
     (* FIXME: This is a quite dummy rearrangement *)
     let r =
-      List.map (fun (i,t,r,p) ->
+      List.map (fun (i,t,kelim,r,p) ->
           let ctors = List.map (fun (id,t,n) -> (id,t),n) r in
           { ind_name = i;
             ind_type = t;
-            ctors; projs = p }) r in
+            ind_kelim = kelim;
+            ind_ctors = ctors; ind_projs = p }) r in
     fun pr ->
     PType (kn,p,r,pr)
   let mkConstant kn ty body = fun pr -> PConstr (kn,ty,body,pr)

test-suite/TypingTests.v

@@ -9,6 +9,7 @@ Import ListNotations.
 
 Require Import Template.TemplateCoqChecker.
 Require Import Template.Typing.
+Require Import Template.Checker.
 Require Import Template.Ast.
 Require Import Template.Template.
 
@@ -18,11 +19,15 @@ Eval vm_compute in typecheck_program idq.
 
 Unset Template Cast Propositions.
 
-
-Definition timpl x y := tProd nAnon x (lift0 1 y).
+Definition timpl x y := tProd nAnon x (LiftSubst.lift0 1 y).
 
 Quote Recursively Definition four := (2 + 2).
 
+Ltac start := unfold type_program; intros; simpl decompose_program;
+  match goal with
+    |- let '(_, _) := (?Σ, ?t) in squash _ => let sigma := fresh in set(sigma:=Σ); hnf; constructor
+  end.
+
 Ltac typecheck := start;
   match goal with
     |- ?Σ ;;; ?Γ |-- ?t : ?T =>
@@ -33,7 +38,7 @@ Ltac infer := start;
     |- ?Σ ;;; ?Γ |-- ?t : ?T => 
     eapply (infer_correct Σ Γ t T);
       let t' := eval vm_compute in (infer Σ Γ t) in
-          change (t' = OfType T); reflexivity
+          change (t' = Checked T); reflexivity
   end.
 
 Example typecheck_four : type_program four natr := ltac:(typecheck).
@@ -53,7 +58,7 @@ Definition test_reduction (p : program) :=
 
 Definition out_typing c :=
   match c with
-  | OfType t => t
+  | Checked t => t
   | TypeError e => tRel 0
   end.
 
@@ -111,7 +116,7 @@ Module Test5.
   Defined.
 
   Time Template Check Plus1.
-
+  (* Too long
   Quote Recursively Definition p_Plus1 := Plus1.
   
   Definition term := Plus1.
@@ -120,9 +125,10 @@ Module Test5.
   (** Check typing *)
   
   (* Yay! Typechecking an actually non-trivial term. (173s) *)
+ 
   Make Definition inferred_type := ltac:(interp_infer ast).
   Definition inferred_type' := Eval cbv delta in inferred_type.
   Print inferred_type'.
-  Check convertible ltac:(term_type term) inferred_type.
+  Check convertible ltac:(term_type term) inferred_type. *)
 End Test5.
 

test-suite/_CoqProject

@@ -18,4 +18,5 @@ bugkncst.v
 evars.v
 proj.v
 cofix.v
-CheckerTest.v
+CheckerTest.v
+TypingTests.v

theories/Checker.v

@@ -522,6 +522,31 @@ Section Typecheck.
       | Some (ConstantDecl _ {| cst_type := ty |}) => ret ty
       |  _ => raise (UndeclaredConstant cst)
     end.
+
+  Definition lookup_ind_type ind i :=
+    match lookup_env Σ ind with
+    | Some (InductiveDecl _ {| ind_bodies := l |}) =>
+      match nth_error l i with
+      | Some body => ret body.(ind_type)
+      | None => raise (UndeclaredInductive (mkInd ind i))
+      end
+    |  _ => raise (UndeclaredInductive (mkInd ind i))
+    end.
+
+  Definition lookup_constructor_type ind i k :=
+    match lookup_env Σ ind with
+    | Some (InductiveDecl _ {| ind_bodies := l |}) =>
+      match nth_error l i with
+      | Some body =>
+        match nth_error body.(ind_ctors) k with
+        | Some (_, ty, _) =>
+          ret (substl (inds ind l) ty)
+        | None => raise (UndeclaredConstructor (mkInd ind i) k)
+        end
+      | None => raise (UndeclaredInductive (mkInd ind i))
+      end
+    |  _ => raise (UndeclaredInductive (mkInd ind i))
+    end.
 
   Fixpoint infer (Γ : context) (t : term) : typing_result term :=
     match t with
@@ -564,30 +589,10 @@ Section Typecheck.
 
     | tConst cst => lookup_constant_type cst
 
-    | tInd (mkInd ind i) =>
-      match lookup_env Σ ind with
-      | Some (InductiveDecl _ {| ind_bodies := l |}) =>
-        match nth_error l i with
-        | Some body => ret body.(ind_type)
-        | None => raise (UndeclaredInductive (mkInd ind i))
-        end
-      |  _ => raise (UndeclaredInductive (mkInd ind i))
-      end
+    | tInd (mkInd ind i) => lookup_ind_type ind i
 
     | tConstruct (mkInd ind i) k =>
-      match lookup_env Σ ind with
-      | Some (InductiveDecl _ {| ind_bodies := l |}) =>
-        match nth_error l i with
-        | Some body =>
-          match nth_error body.(ind_ctors) k with
-          | Some (_, ty, _) =>
-            ret (substl (inds ind l) ty)
-          | None => raise (UndeclaredConstructor (mkInd ind i) k)
-          end
-        | None => raise (UndeclaredInductive (mkInd ind i))
-        end
-      |  _ => raise (UndeclaredInductive (mkInd ind i))
-      end
+      lookup_constructor_type ind i k
 
     | tCase (ind, par) p c brs =>
       ty <- infer Γ c ;;
@@ -655,35 +660,29 @@ Section Typecheck.
         reduce_to_ind Γ t = Checked (i, args') /\
         cumul Σ Γ (mktApp (tInd i) args') (mktApp (tInd i) args).
 
+  Lemma lookup_env_id {id decl} : lookup_env Σ id = Some decl -> id = global_decl_ident decl.
+  Proof.
+    induction Σ; simpl; intros; try discriminate; trivial.
+    revert H. destruct (ident_eq_spec id (global_decl_ident a)). now intros [= ->].
+    apply IHg.
+  Qed.
+
   Lemma lookup_constant_type_declared cst decl (isdecl : declared_constant Σ cst decl) :
     lookup_constant_type cst = Checked decl.(cst_type).
   Proof.
-    unfold lookup_constant_type.
-    destruct isdecl as [d [H H']].
-  Admitted.
-  (*   rewrite H at 1. *)
-
-  (*   induction Σ. simpl. bang. simpl. destruct dec. simpl. *)
-  (*   unfold type_of_constant_decl. simpl. *)
-  (*   simpl in H. pose proof H. rewrite e in H0. *)
-  (*   injection H0 as ->. *)
-  (*   destruct d; auto. bang. *)
-
-  (*   simpl in H. pose proof H. rewrite e in H0. *)
-  (*   specialize (IHg H0). *)
-  (*   rewrite IHg at 1. f_equal. pi. *)
-  (* Qed. *)
-
-  (* Lemma lookup_constant_type_is_declared cst decl : *)
-  (*   lookup_constant_type cst = Checked decl.(cst_type) -> declared_constant Σ cst decl. *)
-  (* Proof. *)
-  (*   unfold lookup_constant_type, declared_constant. *)
-  (*   destruct lookup_env; try discriminate. *)
-  (*   destruct g; intros; try discriminate. destruct c. *)
-  (*   injection H as ->. *)
-  (*   eexists. split; eauto. *)
-  (*   eexists. split; eauto. *)
-  (* Qed. *)
+    unfold lookup_constant_type. red in isdecl. rewrite isdecl. destruct decl. reflexivity.
+  Qed.
+
+  Lemma lookup_constant_type_is_declared cst T :
+    lookup_constant_type cst = Checked T ->
+    { decl | declared_constant Σ cst decl /\ decl.(cst_type) = T }.
+  Proof.
+    unfold lookup_constant_type, declared_constant.
+    destruct lookup_env eqn:Hlook; try discriminate.
+    destruct g eqn:Hg; intros; try discriminate. destruct c.
+    injection H as ->. rewrite (lookup_env_id Hlook). simpl.
+    eexists. split; eauto.
+  Qed.
 
   Lemma eq_ind_refl i i' : eq_ind i i' = true <-> i = i'.
   Admitted.
@@ -801,37 +800,34 @@ Section Typecheck.
   Qed.
 
   Lemma nth_error_Some_safe_nth A (l : list A) n c :
-    nth_error l n = Some c -> { isdecl : _ &
-      safe_nth l (exist _ n isdecl) = c }.
+    forall e : nth_error l n = Some c, safe_nth l (exist _ n (nth_error_isdecl e)) = c.
   Proof.
     intros H.
-    pose proof H.
-    pose proof (nth_error_safe_nth _ _ (nth_error_isdecl H0)).
-    rewrite H in H1.
-    eexists. injection H1 as <-. reflexivity.
+    pose proof (nth_error_safe_nth _ _ (nth_error_isdecl H)).
+    rewrite H in H0 at 1. now injection H0 as ->.
   Qed.
-
 
   Ltac infco := eauto using infer_cumul_correct, infer_type_correct.
+
+  (* Axiom cheat : forall A, A. *)
+  (* Ltac admit := apply cheat. *)
+
   Lemma infer_correct Γ t T :
     infer Γ t = Checked T -> Σ ;;; Γ |-- t : T.
   Proof.
     induction t in Γ, T |- * ; simpl; intros; try discriminate;
       revert H; infers; try solve [econstructor; infco].
 
     - destruct nth_error eqn:Heq; try discriminate.
-      destruct (nth_error_Some_safe_nth _ _ _ _ Heq) as [isdecl <-].
+      pose proof (nth_error_Some_safe_nth _ _ _ _ Heq).
+      destruct H.
       intros [= <-]. constructor.
 
     - admit.
 
     - intros.
-
-      (* pose proof (lookup_constant_type_declared _ (lookup_constant_type_is_declared _ _ H)). *)
-      (* rewrite H in H0 at 1. *)
-      (* injection H0 as ->. tc. *)
-      (* constructor. *)
-      admit.
+      destruct (lookup_constant_type_is_declared _ _ H) as [decl [Hdecl <-]].
+      constructor. auto.
 
     - (* Ind *) admit.
 
@@ -863,9 +859,11 @@ Section Typecheck.
       destruct (nth_error_Some_safe_nth _ _ _ _ Heqo) as [isdecl <-].
       constructor.
   Admitted.
-
+  
 End Typecheck.
 
+Extract Constant infer_correct => "(fun f sigma ctx t ty -> assert false)".
+
 Instance default_fuel : Fuel := { fuel := 2 ^ 18 }.
 
 Fixpoint fresh id env : bool :=

theories/Typing.v

@@ -105,6 +105,11 @@ Definition global_context := list global_decl.
 Definition ident_eq (x y : ident) :=
   if string_dec x y then true else false.
 
+Lemma ident_eq_spec x y : reflect (x = y) (ident_eq x y).
+Proof.
+  unfold ident_eq. destruct string_dec; constructor; auto.
+Qed.
+
 Fixpoint lookup_env (Σ : global_context) (id : ident) : option global_decl :=
   match Σ with
   | nil => None
@@ -792,7 +797,7 @@ Proof.
   destruct m; constructor; [|apply auxm].
   split; apply auxt.
 Defined.
-Axiom cheat : forall A, A.
+
 Lemma term_env_ind' :
   forall P : global_context -> term -> Prop,
     (forall Σ n, P Σ (tRel n)) ->