From 5b94860fab22ed1028e613f6351b3a3ea7e265d1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 27 Sep 2017 12:13:08 +0200 Subject: [PATCH] sorts_family in checker and fix .v files as well w.r.t. change of sort --- src/template_coq.ml4 | 12 +++- test-suite/TypingTests.v | 18 ++++-- test-suite/_CoqProject | 3 +- theories/Checker.v | 124 +++++++++++++++++++-------------------- theories/Typing.v | 7 ++- 5 files changed, 91 insertions(+), 73 deletions(-) diff --git a/src/template_coq.ml4 b/src/template_coq.ml4 index eededc383..f1f7d437e 100644 --- a/src/template_coq.ml4 +++ b/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) diff --git a/test-suite/TypingTests.v b/test-suite/TypingTests.v index c651936bb..33c0760fc 100644 --- a/test-suite/TypingTests.v +++ b/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. diff --git a/test-suite/_CoqProject b/test-suite/_CoqProject index af28606f0..044b096f4 100644 --- a/test-suite/_CoqProject +++ b/test-suite/_CoqProject @@ -18,4 +18,5 @@ bugkncst.v evars.v proj.v cofix.v -CheckerTest.v \ No newline at end of file +CheckerTest.v +TypingTests.v diff --git a/theories/Checker.v b/theories/Checker.v index a2636b2e5..d97c7cedb 100644 --- a/theories/Checker.v +++ b/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,18 +800,18 @@ 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. @@ -820,18 +819,15 @@ Section Typecheck. 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 := diff --git a/theories/Typing.v b/theories/Typing.v index 7b4a761eb..55dcb3305 100644 --- a/theories/Typing.v +++ b/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)) ->