Parameterize over types and identifiers

1 files changed, 318 insertions, 182 deletions

diff --git a/src/Experiments/PartialEvaluationWithLetIn.v b/src/Experiments/PartialEvaluationWithLetIn.v
index d6df6db0c..090abaea9 100644
--- a/src/Experiments/PartialEvaluationWithLetIn.v
+++ b/src/Experiments/PartialEvaluationWithLetIn.v
@@ -12,37 +12,42 @@ Require Import Crypto.Util.Notations.
 *)
 
 Module type.
-  Inductive type := nat | prod (A B : type) | arrow (s d : type).
+  Inductive type (base_type : Type) := base (t : base_type) | arrow (s d : type base_type).
+  Global Arguments base {_}.
+  Global Arguments arrow {_} s d.
 End type.
 Notation type := type.type.
 Delimit Scope etype_scope with etype.
 Bind Scope etype_scope with type.type.
 Infix "->" := type.arrow : etype_scope.
-Infix "*" := type.prod : etype_scope.
+Module base.
+  Module type.
+    Inductive type := nat | prod (A B : type).
+  End type.
+  Notation type := type.type.
+End base.
+Bind Scope etype_scope with base.type.
+Infix "*" := base.type.prod : etype_scope.
 
-
-Fixpoint upperboundT (t : type) : Type
+Fixpoint upperboundT (t : base.type) : Type
   := match t with
-     | type.nat => option nat
-     | type.prod A B => upperboundT A * upperboundT B
-     | type.arrow s d => unit
+     | base.type.nat => option nat
+     | base.type.prod A B => upperboundT A * upperboundT B
      end.
 
 Module expr.
   Section with_var.
-    Context {var : type -> Type}.
+    Context {base_type : Type}.
+    Local Notation type := (type base_type).
+    Context {ident : type -> Type}
+            {var : type -> Type}.
 
     Inductive expr : type -> Type :=
-    | Literal (v : nat) : expr type.nat
+    | Ident {t} (idc : ident t) : expr t
     | Var {t} (v : var t) : expr t
-    | Plus (x y : expr type.nat) : expr type.nat
     | Abs {s d} (f : var s -> expr d) : expr (s -> d)
     | App {s d} (f : expr (s -> d)) (x : expr s) : expr d
-    | Pair {A B} (a : expr A) (b : expr B) : expr (A * B)
-    | Fst {A B} (x : expr (A * B)) : expr A
-    | Snd {A B} (x : expr (A * B)) : expr B
     | LetIn {A B} (x : expr A) (f : var A -> expr B) : expr B
-    | Cast {T} (upper_bound : upperboundT T) (e : expr T) : expr T
     .
   End with_var.
 
@@ -53,23 +58,54 @@ Module expr.
     Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\  x .. y , '//' t").
     Notation "\ x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope.
     Notation "'λ' x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope.
-    Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope.
     Notation "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : expr_scope.
-    Infix "+" := Plus : expr_scope.
-    Notation "' x" := (Literal x) (at level 9, format "' x") : expr_scope.
     Notation "'$' x" := (Var x) (at level 9, format "'$' x") : expr_scope.
+    Notation "' x" := (Ident x) (at level 9, x at level 10, format "' x") : expr_scope.
   End Notations.
 End expr.
 Import expr.Notations.
 Notation expr := expr.expr.
 
+Module ident.
+  Local Notation type := (type base.type).
+  Section with_base.
+    Let type_base (x : base.type) : type := type.base x.
+    Local Coercion type_base : base.type >-> type.
+
+    Inductive ident : type -> Type :=
+    | Literal (v : nat) : ident base.type.nat
+    | Plus : ident (base.type.nat -> base.type.nat -> base.type.nat)
+    | Pair {A B : base.type} : ident (A -> B -> A * B)
+    | Fst {A B} : ident (A * B -> A)
+    | Snd {A B} : ident (A * B -> B)
+    | Cast {T} (upper_bound : upperboundT T) : ident (T -> T)
+    .
+  End with_base.
+
+  Module Export Notations.
+    Delimit Scope ident_scope with ident.
+    Bind Scope ident_scope with ident.
+    Global Arguments expr.Ident {base_type%type ident%function var%function t%etype} idc%ident.
+    Notation "( x , y , .. , z )" := (expr.App (expr.App (expr.Ident Pair) .. (expr.App (expr.App (expr.Ident Pair) x%expr) y%expr) .. ) z%expr) : expr_scope.
+    Notation "x + y" := ('Plus @ x @ y)%expr : expr_scope.
+    Notation "` x" := (Literal x) (at level 9, x at level 10, format "` x") : ident_scope.
+    Notation "` x" := (expr.Ident (Literal x)) (at level 9, x at level 10, format "` x") : expr_scope.
+  End Notations.
+End ident.
+Import ident.Notations.
+Notation ident := ident.ident.
+
 Module UnderLets.
   Section with_var.
-    Context {var : type -> Type}.
+    Context {base_type : Type}.
+    Local Notation type := (type base_type).
+    Context {ident : type -> Type}
+            {var : type -> Type}.
+    Local Notation expr := (@expr base_type ident var).
 
     Inductive UnderLets {T : Type} :=
     | Base (v : T)
-    | UnderLet {A} (x : @expr var A) (f : var A -> UnderLets).
+    | UnderLet {A} (x : expr A) (f : var A -> UnderLets).
 
     Fixpoint splice {A B} (x : @UnderLets A) (e : A -> @UnderLets B) : @UnderLets B
       := match x with
@@ -77,7 +113,7 @@ Module UnderLets.
          | UnderLet A x f => UnderLet x (fun v => @splice _ _ (f v) e)
          end.
 
-    Fixpoint to_expr {t} (x : @UnderLets (@expr var t)) : @expr var t
+    Fixpoint to_expr {t} (x : @UnderLets (expr t)) : expr t
       := match x with
          | Base v => v
          | UnderLet A x f
@@ -93,65 +129,47 @@ Notation "x <-- y ; f" := (UnderLets.splice y (fun x => f%under_lets)) : under_l
 Module partial.
   Import UnderLets.
   Section with_var.
-    Context (var : type -> Type)
-            (stateT : type -> Type)
-            (cast : forall t, stateT t -> @expr var t -> @expr var t)
-            (add_state : stateT type.nat -> stateT type.nat -> stateT type.nat)
-            (fst_state : forall A B, stateT (type.prod A B) -> stateT A)
-            (snd_state : forall A B, stateT (type.prod A B) -> stateT B)
-            (state_of_literal : nat -> stateT type.nat)
-            (pair_state : forall A B, stateT A -> stateT B -> stateT (type.prod A B))
-            (intersect_state : forall A, stateT A -> stateT A -> stateT A)
-            (update_literal_with_state : stateT type.nat -> nat -> nat)
-            (state_of_upperbound : forall T, upperboundT T -> stateT T)
-            (bottom : forall A, stateT A).
+    Context {base_type : Type}.
+    Local Notation type := (type base_type).
+    Let type_base (x : base_type) : type := type.base x.
+    Local Coercion type_base : base_type >-> type.
+    Context {ident : type -> Type}
+            {var : type -> Type}.
+    Local Notation expr := (@expr base_type ident).
+    Local Notation UnderLets := (@UnderLets base_type ident var).
+    Context (base_value : base_type -> Type)
+            (stateT' : base_type -> Type)
+            (cast : forall t, stateT' t -> @expr var t -> @expr var t)
+            (intersect_state : forall A, stateT' A -> stateT' A -> stateT' A)
+            (bottom : forall A, stateT' A)
+            (state_of_base_value : forall t, base_value t -> stateT' t)
+            (base_reify : forall t, base_value t -> @expr var t).
 
     Fixpoint value (t : type)
       := match t with
-         | type.nat as t
-           => stateT t * @expr var t + nat
-         | type.prod A B as t
-           => stateT t * @expr var t + value A * value B
+         | type.base t
+           => stateT' t * @expr var t + base_value t
          | type.arrow s d
-           => value s -> UnderLets var (value d)
+           => value s -> UnderLets (value d)
          end%type.
     Definition value_with_lets (t : type)
-      := UnderLets var (value t).
+      := UnderLets (value t).
 
-    Fixpoint state_of_value {t} : value t -> stateT t
-      := match t return value t -> stateT t with
-         | type.nat
-           => fun v
-              => match v with
-                 | inl (st, _) => st
-                 | inr n => state_of_literal n
-                 end
-         | type.prod A B
-           => fun v
-              => match v with
-                 | inl (st, _) => st
-                 | inr (a, b)
-                   => pair_state
-                        _ _
-                        (@state_of_value A a) (@state_of_value B b)
-                 end
-         | type.arrow s d => fun _ => bottom _
+    Context (interp_ident : forall t, ident t -> value t).
+
+    Definition stateT (t : type)
+      := match t with
+         | type.base t => stateT' t
+         | type.arrow s d => unit
          end.
 
     Fixpoint reify {t} : value t -> @expr var t
-      := match t return value t -> expr t with
-         | type.nat
-           => fun v
-              => match v with
-                 | inl (st, e) => cast _ st e
-                 | inr n => expr.Literal n
-                 end
-         | type.prod A B
+      := match t return value t -> @expr var t with
+         | type.base t
            => fun v
               => match v with
                  | inl (st, e) => cast _ st e
-                 | inr (a, b)
-                   => expr.Pair (@reify _ a) (@reify _ b)
+                 | inr v => base_reify _ v
                  end
          | type.arrow s d
            => fun f => λ x , (UnderLets.to_expr
@@ -159,95 +177,56 @@ Module partial.
                                    Base (@reify _ fx)))
          end%core%expr
     with reflect {t} : @expr var t -> value t
-         := match t return expr t -> value t with
-            | type.nat
-            | type.prod _ _
+         := match t return @expr var t -> value t with
+            | type.base t
               => fun e => inl (bottom _, e)
             | type.arrow s d
               => fun e v
                  => Base (@reflect d (e @ (@reify s v)))%expr
             end.
 
+    Fixpoint state_of_value {t} : value t -> stateT t
+      := match t return value t -> stateT t with
+         | type.base t
+           => fun v
+              => match v with
+                 | inl (st, _) => st
+                 | inr n => state_of_base_value _ n
+                 end
+         | type.arrow s d => fun _ => tt
+         end.
+
     Definition put_state {t} : stateT t -> @expr var t -> value t
       := match t return stateT t -> expr t -> value t with
-         | type.nat
-         | type.prod _ _
+         | type.base t
            => fun st e => inl (st, e)
          | type.arrow s d
-           => fun st e => reflect e
-         end.
-
-    Fixpoint intersect_state_value {t} : stateT t -> value t -> value t
-      := match t return stateT t -> value t -> value t with
-         | type.nat
-           => fun st e
-              => match e with
-                 | inl (st', e) => inl (intersect_state _ st st', e)
-                 | inr v => inr (update_literal_with_state st v)
-                 end
-         | type.prod _ _
-           => fun st e
-              => match e with
-                 | inl (st', e) => inl (intersect_state _ st st', e)
-                 | inr (a, b) => inr (@intersect_state_value _ (fst_state _ _ st) a,
-                                      @intersect_state_value _ (snd_state _ _ st) b)
-                 end
-         | type.arrow s d
-           => fun st e => e
+           => fun _ e => reflect e
          end.
 
     Fixpoint interp {t} (e : @expr value_with_lets t) : value_with_lets t
       := match e in expr.expr t return value_with_lets t with
-         | expr.Literal v => Base (inr v)
+         | expr.Ident t idc => Base (interp_ident t idc)
          | expr.Var t v => v
-         | expr.Plus x y
-           => (x' <-- @interp _ x;
-                 y' <-- @interp _ y;
-                 Base (match x', y' with
-                       | inr xv, inr yv => inr (xv + yv)
-                       | _, _ => put_state
-                                   (add_state (state_of_value x') (state_of_value y'))
-                                   (expr.Plus (@reify type.nat x')
-                                              (@reify type.nat y'))
-                       end))
          | expr.Abs s d f => Base (fun x => @interp d (f (Base x)))
          | expr.App s d f x
            => (x' <-- @interp s x;
                  f' <-- @interp (s -> d)%etype f;
                  f' x')
-         | expr.Pair A B a b
-           => (a' <-- @interp A a;
-                 b' <-- @interp B b;
-                 Base (inr (a', b')))
-         | expr.Fst A B x
-           => (x' <-- @interp _ x;
-                 Base match x' return value _ with
-                      | inl (st, e) => put_state (fst_state _ _ st) (expr.Fst e)
-                      | inr (a, b) => a
-                      end)
-         | expr.Snd A B x
-           => (x' <-- @interp _ x;
-                 Base match x' return value _ with
-                      | inl (st, e) => put_state (snd_state _ _ st) (expr.Snd e)
-                      | inr (a, b) => b
-                      end)
          | expr.LetIn A B x f
            => (x' <-- @interp _ x;
                  UnderLet
                    (reify x')
                    (fun x'v
                     => @interp _ (f (Base (put_state (state_of_value x') (expr.Var x'v))))))
-         | expr.Cast T bound e
-           => (e' <-- @interp _ e;
-                 Base (intersect_state_value (state_of_upperbound _ bound) e'))
          end%under_lets.
 
-    Definition eval {t} (e : @expr value_with_lets t) : @expr var t
+    Definition eval {t} (e : @expr value_with_lets t) : expr t
       := UnderLets.to_expr (e' <-- interp e; Base (reify e')).
 
     Definition eval_with_bound {s d} (e : @expr value_with_lets (s -> d))
                (st : stateT s)
-      : @expr var (s -> d)
+      : expr (s -> d)
       := UnderLets.to_expr
            (e' <-- interp e;
               Base
@@ -257,75 +236,232 @@ Module partial.
                          (e'' <-- e' (put_state st (expr.Var x));
                             Base (reify e''))))).
   End with_var.
+
+  Module ident.
+    Section with_var.
+      Local Notation type := (type base.type).
+      Let type_base (x : base.type) : type := type.base x.
+      Local Coercion type_base : base.type >-> type.
+      Context {var : type -> Type}.
+      Local Notation expr := (@expr base.type ident).
+      Local Notation UnderLets := (@UnderLets base.type ident var).
+      Context (stateT' : base.type -> Type)
+              (cast : forall t, stateT' t -> @expr var t -> @expr var t)
+              (add_state : stateT' base.type.nat -> stateT' base.type.nat -> stateT' base.type.nat)
+              (fst_state : forall A B, stateT' (base.type.prod A B) -> stateT' A)
+              (snd_state : forall A B, stateT' (base.type.prod A B) -> stateT' B)
+              (state_of_literal : nat -> stateT' base.type.nat)
+              (pair_state : forall A B, stateT' A -> stateT' B -> stateT' (base.type.prod A B))
+              (intersect_state : forall A, stateT' A -> stateT' A -> stateT' A)
+              (update_literal_with_state : stateT' base.type.nat -> nat -> nat)
+              (state_of_upperbound : forall T, upperboundT T -> stateT' T)
+              (bottom : forall A, stateT' A).
+
+      Fixpoint base_value (t : base.type)
+        := match t return Type with
+           | base.type.nat as t
+             => nat
+           | base.type.prod A B as t
+             => (stateT' A * @expr var A + base_value A) * (stateT' B * @expr var B + base_value B)
+           end%type.
+
+      Fixpoint state_of_base_value {t} : base_value t -> stateT' t
+        := match t return base_value t -> stateT' t with
+           | base.type.nat => state_of_literal
+           | base.type.prod A B
+             => fun '(a, b)
+                => let sta := match a with
+                              | inl (st, _) => st
+                              | inr a' => @state_of_base_value A a'
+                              end in
+                   let stb := match b with
+                              | inl (st, _) => st
+                              | inr b' => @state_of_base_value B b'
+                              end in
+                   pair_state _ _ sta stb
+           end.
+
+      Fixpoint base_reify {t} : base_value t -> @expr var t
+        := match t return base_value t -> expr t with
+           | base.type.nat
+             => fun v => expr.Ident (ident.Literal v)
+           | base.type.prod A B
+             => fun '(a, b)
+                => let ea := match a with
+                             | inl (st, e) => cast _ st e
+                             | inr v => @base_reify _ v
+                             end in
+                   let eb := match b with
+                             | inl (st, e) => cast _ st e
+                             | inr v => @base_reify _ v
+                             end in
+                   ('ident.Pair @ ea @ eb)%expr
+           end.
+
+      Fixpoint intersect_state_base_value {t} : stateT' t -> base_value t -> base_value t
+        := match t return stateT' t -> base_value t -> base_value t with
+           | base.type.nat => update_literal_with_state
+           | base.type.prod _ _
+             => fun st '(a, b)
+                => let sta := fst_state _ _ st in
+                   let stb := snd_state _ _ st in
+                   let a' := match a with
+                             | inl (sta', e) => inl (intersect_state _ sta sta', e)
+                             | inr v => inr (@intersect_state_base_value _ sta v)
+                             end in
+                   let b' := match b with
+                             | inl (stb', e) => inl (intersect_state _ stb stb', e)
+                             | inr v => inr (@intersect_state_base_value _ stb v)
+                             end in
+                   (a', b')
+           end.
+
+
+      Local Notation value := (@value base.type ident var base_value stateT').
+      Local Notation stateT := (@stateT base.type stateT').
+
+      Definition intersect_state_value {t} : stateT t -> value t -> value t
+        := match t with
+           | type.base t
+             => fun st e
+                => match e with
+                   | inl (st', e) => inl (intersect_state _ st st', e)
+                   | inr v => inr (intersect_state_base_value st v)
+                   end
+           | type.arrow s d => fun _ e => e
+           end.
+
+      Local Notation state_of_value := (@state_of_value base.type ident var base_value stateT' (@state_of_base_value)).
+      Local Notation reify := (@reify base.type ident var base_value stateT' cast bottom (@base_reify)).
+
+      Definition interp {t} (idc : ident t) : value t
+        := match idc in ident.ident t return value t with
+           | ident.Literal v => inr v
+           | ident.Plus
+             => fun x'
+                => Base
+                     (fun y'
+                      => Base
+                           match x', y' with
+                           | inr xv, inr yv => inr (xv + yv)
+                           | _, _ => inl
+                                       (add_state (@state_of_value base.type.nat x')
+                                                  (@state_of_value base.type.nat y'),
+                                        ('ident.Plus
+                                           @ (@reify base.type.nat x')
+                                           @ (@reify base.type.nat y'))%expr)
+                           end)
+           | ident.Pair A B
+             => fun a'
+                => Base
+                     (fun b'
+                      => Base
+                           (inr (a', b')))
+           | ident.Fst A B
+             => fun x'
+                => Base
+                     match x' return value (type.base _) with
+                     | inl (st, e) => inl (fst_state _ _ st, ('ident.Fst @ e)%expr)
+                     | inr (a, b) => a
+                     end
+           | ident.Snd A B
+             => fun x'
+                => Base
+                     match x' return value (type.base _) with
+                     | inl (st, e) => inl (snd_state _ _ st, ('ident.Snd @ e)%expr)
+                     | inr (a, b) => b
+                     end
+           | ident.Cast T bound
+             => fun e'
+                => Base (intersect_state_value (t:=T) (state_of_upperbound _ bound) e')
+           end.
+
+      Local Notation value_with_lets := (@value_with_lets base.type ident var base_value stateT').
+
+      Definition eval {t} (e : @expr value_with_lets t) : @expr var t
+        := @eval base.type ident var base_value stateT' cast bottom (@state_of_base_value) (@base_reify) (@interp) t e.
+
+      Definition eval_with_bound {s d} (e : @expr value_with_lets (s -> d))
+                 (st : stateT s)
+        : expr (s -> d)
+        := @eval_with_bound base.type ident var base_value stateT' cast bottom (@state_of_base_value) (@base_reify) (@interp) s d e st.
+    End with_var.
+  End ident.
 End partial.
 
-Local Notation stateT := upperboundT.
-Definition cast {var} t (st : stateT t) (e : @expr var t) : @expr var t
-  := expr.Cast st e.
-Fixpoint bottom T : stateT T
-  := match T return stateT T with
-     | type.nat => None
-     | type.prod A B => (bottom _, bottom _)
-     | type.arrow s d => tt
-     end.
-Definition add_state : stateT type.nat -> stateT type.nat -> stateT type.nat
-  := fun x y
-     => match x, y with
-        | Some x', Some y' => Some (x' + y')
-        | _, _ => None
-        end.
-Definition fst_state : forall A B : type, stateT (A * B)%etype -> stateT A
-  := fun _ _ => @fst _ _.
-Definition snd_state : forall A B : type, stateT (A * B)%etype -> stateT B
-  := fun _ _ => @snd _ _.
-Definition state_of_literal : nat -> stateT type.nat
-  := @Some _.
-Definition pair_state : forall A B, stateT A -> stateT B -> stateT (type.prod A B)
-  := fun _ _ => @pair _ _.
-Fixpoint intersect_state A : stateT A -> stateT A -> stateT A
-  := match A return stateT A -> stateT A -> stateT A with
-     | type.nat
-       => fun x y
-          => match x, y with
-             | Some x', Some y' => Some (Nat.min x' y')
-             | Some x', None | None, Some x' => Some x'
-             | None, None => None
-             end
-     | type.prod A B
-       => fun '(x, y) '(x', y') => (@intersect_state _ x x', @intersect_state _ y y')
-     | type.arrow s d => fun _ _ => tt
-     end.
-Axiom evil : nat -> nat.
-Definition update_literal_with_state : stateT type.nat -> nat -> nat
-  := fun upperbound n
-     => match upperbound with
+Section specialized.
+  Local Notation stateT' := upperboundT.
+  Local Notation stateT := (@partial.stateT base.type stateT').
+  Notation expr := (@expr base.type ident).
+  Local Notation type := (type base.type).
+  Let type_base (x : base.type) : type := type.base x.
+  Local Coercion type_base : base.type >-> type.
+  Definition cast {var} t (st : stateT' t) (e : @expr var t) : @expr var t
+    := ('ident.Cast st @ e)%expr.
+  Fixpoint bottom T : stateT' T
+    := match T return stateT' T with
+       | base.type.nat => None
+       | base.type.prod A B => (bottom _, bottom _)
+       end.
+  Definition add_state : stateT' base.type.nat -> stateT' base.type.nat -> stateT' base.type.nat
+    := fun x y
+       => match x, y with
+          | Some x', Some y' => Some (x' + y')
+          | _, _ => None
+          end.
+  Definition fst_state : forall A B : base.type, stateT' (A * B)%etype -> stateT' A
+    := fun _ _ => @fst _ _.
+  Definition snd_state : forall A B : base.type, stateT' (A * B)%etype -> stateT' B
+    := fun _ _ => @snd _ _.
+  Definition state_of_literal : nat -> stateT' base.type.nat
+    := @Some _.
+  Definition pair_state : forall A B, stateT' A -> stateT' B -> stateT' (base.type.prod A B)
+    := fun _ _ => @pair _ _.
+  Fixpoint intersect_state A : stateT' A -> stateT' A -> stateT' A
+    := match A return stateT' A -> stateT' A -> stateT' A with
+       | base.type.nat
+         => fun x y
+            => match x, y with
+               | Some x', Some y' => Some (Nat.min x' y')
+               | Some x', None | None, Some x' => Some x'
+               | None, None => None
+               end
+       | base.type.prod A B
+         => fun '(x, y) '(x', y') => (@intersect_state _ x x', @intersect_state _ y y')
+       end.
+  Axiom evil : nat -> nat.
+  Definition update_literal_with_state : stateT' base.type.nat -> nat -> nat
+    := fun upperbound n
+       => match upperbound with
         | Some upperbound'
           => if Nat.leb n upperbound' then n else evil n
         | None => n
         end.
-Definition state_of_upperbound : forall T, upperboundT T -> stateT T
-  := fun _ x => x.
+  Definition state_of_upperbound : forall T, upperboundT T -> stateT' T
+    := fun _ x => x.
 
-Print partial.eval.
+  Print partial.ident.eval.
 
-Definition eval {var} {t} (e : @expr _ t) : expr t
-  := @partial.eval
-              var stateT cast add_state fst_state snd_state state_of_literal pair_state intersect_state update_literal_with_state state_of_upperbound bottom t e.
-Definition eval_with_bound {var} {s d} (e : @expr _ (s -> d)) (bound : stateT s) : expr (s -> d)
-  := @partial.eval_with_bound
-              var stateT cast add_state fst_state snd_state state_of_literal pair_state intersect_state update_literal_with_state state_of_upperbound bottom s d e bound.
+  Definition eval {var} {t} (e : @expr _ t) : expr t
+    := (@partial.ident.eval)
+         var stateT' cast add_state fst_state snd_state state_of_literal pair_state intersect_state update_literal_with_state state_of_upperbound bottom t e.
+  Definition eval_with_bound {var} {s d} (e : @expr _ (s -> d)) (bound : stateT s) : expr (s -> d)
+    := (@partial.ident.eval_with_bound)
+         var stateT cast add_state fst_state snd_state state_of_literal pair_state intersect_state update_literal_with_state state_of_upperbound bottom s d e bound.
 
-Import expr.
-Compute eval (Fst (LetIn (Literal 10) (fun x => Pair (Var x) (Var x)))).
+  Import expr.
+  Import ident.
+  Compute eval ('Fst @ (expr_let x := `10 in ($x, $x)))%expr.
 
-Compute eval ((\ x , expr_let y := '5 in Fst $x + (Fst $x + ($y + $y)))
-                @ ('1, '1))%expr.
+  Compute eval ((\ x , expr_let y := `5 in 'Fst @ $x + ('Fst @ $x + ($y + $y)))
+                  @ (`1, `1))%expr.
 
-Compute eval ((\ x , expr_let y := '5 in $y + ($y + (Fst $x + Snd $x)))
-                @ ('1, '7))%expr.
+  Compute eval ((\ x , expr_let y := `5 in $y + ($y + ('Fst @ $x + 'Snd @ $x)))
+                  @ (`1, `7))%expr.
 
 
-Eval cbv in eval_with_bound
-              (\z , ((\ x , expr_let y := '5 in $y + ($z + (Fst $x + Snd $x)))
-                       @ ('1, '7)))%expr
-              (Some 100).
+  Eval cbv in eval_with_bound
+                (\z , ((\ x , expr_let y := `5 in $y + ($z + ('Fst @ $x + 'Snd @ $x)))
+                         @ (`1, `7)))%expr
+                (Some 100).
+End specialized.