Skip to content

Commit

Permalink
coq: Remove some commented-out code
Browse files Browse the repository at this point in the history
  • Loading branch information
@cpitclaudel
cpitclaudel committed Oct 31, 2019
1 parent 52c6086 commit 45460fb
Showing 1 changed file with 0 additions and 174 deletions.
174 changes: 0 additions & 174 deletions coq/TypeInference.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)

0 comments on commit 45460fb

Please sign in to comment.