From 45460fb97897b36508bef3e55187780eeef970cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Wed, 30 Oct 2019 22:46:12 -0400 Subject: [PATCH] coq: Remove some commented-out code --- coq/TypeInference.v | 174 -------------------------------------------- 1 file changed, 174 deletions(-) diff --git a/coq/TypeInference.v b/coq/TypeInference.v index e27b92e2..d556fd24 100644 --- a/coq/TypeInference.v +++ b/coq/TypeInference.v @@ -203,177 +203,3 @@ Section TypeInference. end. End Scheduler. End TypeInference. - -(* Hint Resolve (@env_related_putenv _ _ _ GammaEnv): types. *) -(* Hint Resolve fenv_related_putenv: types. *) -(* Hint Constructors HasType : types. *) -(* Hint Extern 0 => unfold id : types. *) - -(* Ltac t := *) -(* repeat match goal with *) -(* | _ => reflexivity *) -(* | _ => progress cleanup_step *) -(* | [ H: opt_bind ?x _ = Some _ |- _ ] => *) -(* destruct x eqn:?; cbn in H; [ | discriminate] *) -(* | [ H: match ?x with _ => _ end = Some _ |- _ ] => *) -(* destruct x eqn:? *) -(* | [ H: env_related (Env := ?Env) ?f ?tenv ?env, *) -(* H': getenv ?env ?k = Some ?v |- _ ] => *) -(* pose_once (and_fst H k v) H' *) -(* | [ H: forall Gamma gamma tau, _ -> _ = Some _ -> _, *) -(* H': type_action ?Gamma ?r = Some ?tau |- _ ] => *) -(* specialize (H Gamma _ tau ltac:(eauto with types) H') *) -(* | [ H: MaxType ?R ?Sigma ?Gamma ?r ?tau |- _ ] => *) -(* pose_once (MaxType_HasType R Sigma Gamma r tau) H *) -(* | _ => solve [econstructor] || econstructor; solve [eauto 5 with types] *) -(* end. *) - -(* Lemma type_action_correct_call: *) -(* forall sigma v, *) -(* env_related id v R -> *) -(* env_related id sigma Sigma -> *) -(* forall args argSizes, *) -(* length args = length argSizes -> *) -(* forall Gamma gamma, *) -(* env_related id gamma Gamma -> *) -(* List.Forall *) -(* (fun r : rule var_t fn_t => *) -(* forall Gamma gamma tau, *) -(* env_related id gamma Gamma -> type_action Gamma r = Some tau -> MaxType v sigma gamma r tau) args -> *) -(* fold_right2 *) -(* (fun arg argSize acc => *) -(* acc && *) -(* match type_action Gamma arg with *) -(* | Some tau => if type_le_dec (bits_t argSize) tau then true else false *) -(* | None => false *) -(* end) true args argSizes = true -> *) -(* fold_right2 *) -(* (fun (arg : rule var_t fn_t) (argSize : nat) (acc : Prop) => acc /\ HasType v sigma gamma arg (bits_t argSize)) *) -(* True args argSizes. *) -(* Proof. *) -(* induction args; destruct argSizes; cbn in *; *) -(* inversion 1; intros ? ? ?; inversion 1; subst; intros Heq. *) -(* - eauto. *) -(* - destruct type_action eqn:?; *) -(* apply andb_prop in Heq; repeat cleanup_step. *) -(* destruct type_le_dec; try discriminate. *) -(* eauto using MaxType_HasType. *) -(* Qed. *) - -(* Lemma type_action_correct : *) -(* forall sigma v, *) -(* env_related id v R -> *) -(* env_related id sigma Sigma -> *) -(* forall (r: rule var_t fn_t) (Gamma: GammaEnv.(env_t)) gamma (tau: type), *) -(* env_related id gamma Gamma -> *) -(* type_action Gamma r = Some tau -> *) -(* MaxType v sigma gamma r tau. *) -(* Proof. *) -(* induction r using rule_ind'; cbn; intros; t. *) - -(* econstructor; eauto. *) -(* eapply fold_right2_forall2; *) -(* eauto using type_action_correct_call. *) -(* Qed. *) - -(* Lemma forall2_cons_inv {A B} (P: A -> B -> Prop) : *) -(* forall a b la lb, *) -(* forall2 P (a :: la) (b :: lb) -> *) -(* P a b /\ forall2 P la lb. *) -(* Proof. *) -(* intros * H; apply forall2_fold_right2 in H; destruct H as (H & ?). *) -(* apply fold_right2_forall2 in H; intuition. *) -(* Qed. *) - -(* Ltac tcomplete_step := *) -(* match goal with *) -(* | _ => progress subst *) -(* | _ => progress intros *) -(* | [ H: fn ?gamma ?k ?v, H': fenv_related ?gamma ?Gamma |- _ ] => *) -(* try pose_once H' k v; *) -(* match goal with *) -(* | [ H'': fn gamma k v <-> getenv Gamma k = Some v |- _ ] => *) -(* pose_once (and_fst H'') H *) -(* end *) -(* | [ H: HasType _ _ _ _ _ |- _ ] => *) -(* apply HasType_MaxType in H; destruct H as (? & ? & ?) *) -(* | [ H: ?x = Some _ |- opt_bind ?x _ = _ ] => *) -(* rewrite H; cbn *) -(* | [ H: (forall _ _ , _ -> forall _, _ -> type_action _ ?r = Some _) |- *) -(* opt_bind (type_action _ ?r) _ = Some _ ] => *) -(* erewrite H by eauto with types; cbn *) -(* | [ H: type_le ?x ?y |- context[type_le_dec ?x ?y] ] => *) -(* destruct type_le_dec; try tauto *) -(* | _ => cleanup_step *) -(* end. *) - -(* Lemma type_action_complete_call: *) -(* forall (sigma : fenv fn_t ExternalSignature) (v : fenv nat nat) (args : list (rule var_t fn_t)) argSizes, *) -(* length args = length argSizes -> *) -(* List.Forall *) -(* (fun r : rule var_t fn_t => *) -(* forall (gamma : fenv var_t type) (tau : type), *) -(* MaxType v sigma gamma r tau -> *) -(* forall Gamma : env_t GammaEnv, fenv_related gamma Gamma -> type_action Gamma r = Some tau) args -> *) -(* forall (gamma : fenv var_t type) (Gamma : env_t GammaEnv), *) -(* forall2 (fun (arg : rule var_t fn_t) (argSize : nat) => HasType v sigma gamma arg (bits_t argSize)) args argSizes -> *) -(* fenv_related gamma Gamma -> *) -(* forall b : bool, *) -(* fold_right2 *) -(* (fun (arg : rule var_t fn_t) (argSize : nat) (acc : bool) => *) -(* acc && *) -(* match type_action Gamma arg with *) -(* | Some tau0 => if type_le_dec (bits_t argSize) tau0 then true else false *) -(* | None => false *) -(* end) b args argSizes = b. *) -(* Proof. *) -(* induction args; cbn; destruct argSizes; inversion 1; intros HForall * Hforall2 **. *) -(* - reflexivity. *) -(* - inversion HForall as [ | x l Hinfer HForall']; subst. *) - -(* apply forall2_cons_inv in Hforall2. *) - -(* repeat tcomplete_step. *) -(* erewrite Hinfer; eauto. *) -(* repeat tcomplete_step. *) -(* rewrite Bool.andb_true_r. *) -(* eauto. *) -(* Qed. *) - -(* Lemma type_action_complete : *) -(* forall sigma v, *) -(* fenv_related v R -> *) -(* fenv_related sigma Sigma -> *) -(* forall (r: rule var_t fn_t) gamma (tau: type), *) -(* MaxType v sigma gamma r tau -> *) -(* forall (Gamma: GammaEnv.(env_t)), *) -(* fenv_related gamma Gamma -> *) -(* type_action Gamma r = Some tau. *) -(* Proof. *) -(* induction r using rule_ind'; cbn; inversion 1; *) -(* repeat tcomplete_step; eauto using f_equal with types. *) - -(* - destruct PeanoNat.Nat.eq_dec; try tauto. *) -(* erewrite type_action_complete_call; eauto. *) -(* Qed. *) - -(* Theorem TypeInference : *) -(* forall Gamma (r: rule var_t fn_t), *) -(* match type_action Gamma r with *) -(* | Some tau => HasType (tenv_of_env id R) (tenv_of_env id Sigma) (tenv_of_env id Gamma) r tau *) -(* | None => forall tau, not (HasType (tenv_of_env id R) (tenv_of_env id Sigma) (tenv_of_env id Gamma) r tau) *) -(* end. *) -(* Proof. *) -(* intros; destruct type_action eqn:?. *) -(* - eapply MaxType_HasType. *) -(* + eapply type_action_correct; *) -(* try eapply tenv_of_env_related; eauto. *) -(* + eauto with types. *) -(* - intros tau Habs. *) -(* eapply HasType_MaxType in Habs. *) -(* destruct Habs as (? & Habs & Hle). *) -(* eapply type_action_complete in Habs; *) -(* try eapply tenv_of_env_frelated. *) -(* congruence. *) -(* Qed. *) -(* End TypeInference. *)