Removed some old code for ANF that is (a) unused, and (b) places undue requirements on expressions.

ChoreographyCompiler.v

@@ -251,13 +251,13 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
                | [ _ : ConExprMerge E1 E4 = None |- _ ] => fail
                | _ => pose proof (MergeAssocNone E1 E2 E3 E4 H1 H2)
                end
-             | [ H : C.equiv ?C1 ?C2 |- context[C.IsFunctionOK ?C2]] =>
-               rewrite (C.IsFunctionOKEquiv C1 C2 H)
-             | [ |- context[C.IsFunctionOK ?C]] =>
-               lazymatch goal with
-               | [ H: C.IsFunctionOK C = _ |- _ ] => rewrite H
-               | _ => let eq := fresh "eq" in destruct (C.IsFunctionOK C) eqn:eq
-               end
+             (* | [ H : C.equiv ?C1 ?C2 |- context[C.IsFunctionOK ?C2]] => *)
+             (*   rewrite (C.IsFunctionOKEquiv C1 C2 H) *)
+             (* | [ |- context[C.IsFunctionOK ?C]] => *)
+             (*   lazymatch goal with *)
+             (*   | [ H: C.IsFunctionOK C = _ |- _ ] => rewrite H *)
+             (*   | _ => let eq := fresh "eq" in destruct (C.IsFunctionOK C) eqn:eq *)
+             (*   end *)
              end.
   Qed.        
 

Expression.v

@@ -104,15 +104,15 @@ Module Type Expression.
   Parameter ExprClosedAfterStep : forall  e1 e2 n,
       ExprStep e1 e2 -> ExprClosedBelow n e1 -> ExprClosedBelow n e2.
 
-  Parameter ExprOpenVal : Expr -> Prop.
-  Parameter OpenValRename :
-    forall e ξ, ExprOpenVal e -> ExprOpenVal (e ⟨e|ξ⟩).
-  Parameter OpenValSubst :
-    forall e σ, ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e|σ]).
-  Parameter OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e.
-  Parameter ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e.
-  Parameter VarToOpenVal : forall n, ExprOpenVal (ExprVar n).
-  Parameter NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2.
-  Parameter IsOpenVal : Expr -> bool.
-  Parameter IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e.
+  (* Parameter ExprOpenVal : Expr -> Prop. *)
+  (* Parameter OpenValRename : *)
+  (*   forall e ξ, ExprOpenVal e -> ExprOpenVal (e ⟨e|ξ⟩). *)
+  (* Parameter OpenValSubst : *)
+  (*   forall e σ, ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e|σ]). *)
+  (* Parameter OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e. *)
+  (* Parameter ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e. *)
+  (* Parameter VarToOpenVal : forall n, ExprOpenVal (ExprVar n). *)
+  (* Parameter NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2. *)
+  (* Parameter IsOpenVal : Expr -> bool. *)
+  (* Parameter IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e. *)
 End Expression.

LambdaCalc.v

@@ -54,14 +54,14 @@ Module LambdaCalc <: Expression.
   | AbsVal : forall (τ : SimpleType) (e : LC), LCClosedBelow 1 e -> LCVal (abs τ e).
   Definition ExprVal := LCVal.
 
-  Inductive LCOpenVal : LC -> Prop :=
-  | varOVal : forall n, LCOpenVal (var n)
-  | ttOVal  : LCOpenVal ttLC
-  | ffOVal  : LCOpenVal ffLC
-  | zeroOVal : LCOpenVal zero
-  | succOVal : forall e : Expr, LCOpenVal e -> LCOpenVal (succ e)
-  | AbsOVal : forall (τ : SimpleType) (e : LC), LCOpenVal (abs τ e).
-  Definition ExprOpenVal := LCOpenVal.
+  (* Inductive LCOpenVal : LC -> Prop := *)
+  (* | varOVal : forall n, LCOpenVal (var n) *)
+  (* | ttOVal  : LCOpenVal ttLC *)
+  (* | ffOVal  : LCOpenVal ffLC *)
+  (* | zeroOVal : LCOpenVal zero *)
+  (* | succOVal : forall e : Expr, LCOpenVal e -> LCOpenVal (succ e) *)
+  (* | AbsOVal : forall (τ : SimpleType) (e : LC), LCOpenVal (abs τ e). *)
+  (* Definition ExprOpenVal := LCOpenVal. *)
 
   Lemma ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
   Proof.
@@ -377,65 +377,65 @@ Module LambdaCalc <: Expression.
 
   Theorem boolSeperation : tt <> ff. discriminate. Qed.
 
-  Theorem OpenValRename : forall e ξ, ExprOpenVal e -> ExprOpenVal (e ⟨e|ξ⟩).
-  Proof using.
-    intro e; induction e; cbn; intros ξ val_e; inversion val_e; subst;
-      constructor; auto.
-    apply IHe; auto.
-  Qed.
+  (* Theorem OpenValRename : forall e ξ, ExprOpenVal e -> ExprOpenVal (e ⟨e|ξ⟩). *)
+  (* Proof using. *)
+  (*   intro e; induction e; cbn; intros ξ val_e; inversion val_e; subst; *)
+  (*     constructor; auto. *)
+  (*   apply IHe; auto. *)
+  (* Qed. *)
   
-  Theorem OpenValSubst : forall e σ,
-      ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e| σ]).
-  Proof using.
-    intro e; induction e; cbn; intros σ val_e val_σ; auto; inversion val_e; subst.
-    constructor; apply IHe; auto.
-    constructor.
-  Qed.
-
-  Theorem OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e.
-  Proof using.
-    intro e; induction e; cbn; intros σ val; inversion val; subst; constructor.
-    eapply IHe; eauto.
-  Qed.
-
-  Theorem ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e.
-  Proof using.
-    intro e; induction e; intro val; inversion val; subst; constructor.
-    apply IHe; auto.
-  Qed.
-
-  Theorem VarToOpenVal : forall n, ExprOpenVal (ExprVar n).
-  Proof using.
-    intro n; constructor.
-  Qed.
-
-  Theorem NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2.
-  Proof using.
-    intros e1; induction e1; intros val e2 step; inversion val; subst;
-      inversion step; subst.
-    apply IHe1 in H1; auto.
-  Qed.
-
-  Fixpoint IsOpenVal (e : Expr) : bool :=
-    match e with
-    | var x => true
-    | ttLC => true
-    | ffLC => true
-    | zero => true
-    | succ e => IsOpenVal e
-    | fixP x => false
-    | ite x x0 x1 => false
-    | app x x0 => false
-    | abs x x0 => true
-    end.
-
-  Theorem IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e.
-  Proof using.
-    intro e; induction e; cbn; split; intro H; auto; try discriminate; try (inversion H; fail).
-    all: try (constructor; auto; fail).
-    - apply IHe in H; constructor; auto.
-    - inversion H; subst. apply IHe in H1; auto.
-  Qed.
+  (* Theorem OpenValSubst : forall e σ, *)
+  (*     ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e| σ]). *)
+  (* Proof using. *)
+  (*   intro e; induction e; cbn; intros σ val_e val_σ; auto; inversion val_e; subst. *)
+  (*   constructor; apply IHe; auto. *)
+  (*   constructor. *)
+  (* Qed. *)
+
+  (* Theorem OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e. *)
+  (* Proof using. *)
+  (*   intro e; induction e; cbn; intros σ val; inversion val; subst; constructor. *)
+  (*   eapply IHe; eauto. *)
+  (* Qed. *)
+
+  (* Theorem ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e. *)
+  (* Proof using. *)
+  (*   intro e; induction e; intro val; inversion val; subst; constructor. *)
+  (*   apply IHe; auto. *)
+  (* Qed. *)
+
+  (* Theorem VarToOpenVal : forall n, ExprOpenVal (ExprVar n). *)
+  (* Proof using. *)
+  (*   intro n; constructor. *)
+  (* Qed. *)
+
+  (* Theorem NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2. *)
+  (* Proof using. *)
+  (*   intros e1; induction e1; intros val e2 step; inversion val; subst; *)
+  (*     inversion step; subst. *)
+  (*   apply IHe1 in H1; auto. *)
+  (* Qed. *)
+
+  (* Fixpoint IsOpenVal (e : Expr) : bool := *)
+  (*   match e with *)
+  (*   | var x => true *)
+  (*   | ttLC => true *)
+  (*   | ffLC => true *)
+  (*   | zero => true *)
+  (*   | succ e => IsOpenVal e *)
+  (*   | fixP x => false *)
+  (*   | ite x x0 x1 => false *)
+  (*   | app x x0 => false *)
+  (*   | abs x x0 => true *)
+  (*   end. *)
+
+  (* Theorem IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e. *)
+  (* Proof using. *)
+  (*   intro e; induction e; cbn; split; intro H; auto; try discriminate; try (inversion H; fail). *)
+  (*   all: try (constructor; auto; fail). *)
+  (*   - apply IHe in H; constructor; auto. *)
+  (*   - inversion H; subst. apply IHe in H1; auto. *)
+  (* Qed. *)
 
   Lemma ExprRenameClosedBelow : forall e n ξ m,
       (forall k, k < n -> ξ k < m) ->