Revert "WIP with andres, not working pattern language"

This reverts commit 2fcf4cd6aabebb3b68cc0a807e5d7c78e9142cb5.

1 files changed, 74 insertions, 280 deletions

diff --git a/src/Experiments/PartialEvaluationWithLetIn.v b/src/Experiments/PartialEvaluationWithLetIn.v
index 5bcfb2d27..7b854af21 100644
--- a/src/Experiments/PartialEvaluationWithLetIn.v
+++ b/src/Experiments/PartialEvaluationWithLetIn.v
@@ -1,4 +1,3 @@
-Require Import Coq.Lists.List.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Notations.
 
@@ -42,82 +41,13 @@ Bind Scope etype_scope with type.type.
 Infix "->" := type.arrow : etype_scope.
 Module base.
   Module type.
-    Inductive type := nat | prod (A B : type) | list (A : 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 : base.type) : Type
-  := match t with
-     | base.type.nat => option nat
-     | base.type.prod A B => upperboundT A * upperboundT B
-     | base.type.list A => option (list (upperboundT A))
-     end.
-
-Module expr.
-  Section with_var.
-    Context {base_type : Type}.
-    Local Notation type := (type base_type).
-    Context {ident : type -> Type}
-            {var : type -> Type}.
-
-    Inductive expr : type -> Type :=
-    | Ident {t} (idc : ident t) : expr t
-    | Var {t} (v : var t) : expr t
-    | Abs {s d} (f : var s -> expr d) : expr (s -> d)
-    | App {s d} (f : expr (s -> d)) (x : expr s) : expr d
-    | LetIn {A B} (x : expr A) (f : var A -> expr B) : expr B
-    .
-  End with_var.
-
-  Module Export Notations.
-    Delimit Scope expr_scope with expr.
-    Bind Scope expr_scope with expr.
-    Infix "@" := App : expr_scope.
-    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 "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : 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 UnderLets.
-  Section with_var.
-    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 A) (f : var A -> UnderLets).
-
-    Fixpoint splice {A B} (x : @UnderLets A) (e : A -> @UnderLets B) : @UnderLets B
-      := match x with
-         | Base v => e v
-         | UnderLet A x f => UnderLet x (fun v => @splice _ _ (f v) e)
-         end.
-
-    Fixpoint to_expr {t} (x : @UnderLets (expr t)) : expr t
-      := match x with
-         | Base v => v
-         | UnderLet A x f
-           => expr.LetIn x (fun v => @to_expr _ (f v))
-         end.
-  End with_var.
-  Global Arguments UnderLets : clear implicits.
-End UnderLets.
-Delimit Scope under_lets_scope with under_lets.
-Bind Scope under_lets_scope with UnderLets.UnderLets.
-Notation "x <-- y ; f" := (UnderLets.splice y (fun x => f%under_lets)) : under_lets_scope.
-
 Module parametric.
   Local Notation einterp := type.interp.
   Module type.
@@ -149,16 +79,14 @@ Module parametric.
   Local Notation btype := base.type.type.
   Local Notation bnat := base.type.nat.
   Local Notation bprod := base.type.prod.
-  Local Notation blist := base.type.list.
   Module base.
     Module type.
-      Inductive type := nat | prod (A B : type) | list (A : type) | var_with_subst (subst : btype).
+      Inductive type := nat | prod (A B : type) | var_with_subst (subst : btype).
 
       Fixpoint subst (t : type) : btype
         := match t with
            | nat => bnat
            | prod A B => bprod (subst A) (subst B)
-           | list A => blist (subst A)
            | var_with_subst s => s
            end.
 
@@ -169,7 +97,6 @@ Module parametric.
           := match t with
              | nat => Datatypes.nat
              | prod A B => interp A * interp B
-             | list A => Datatypes.list (interp A)
              | var_with_subst s => base_interp s
              end%type.
       End interp.
@@ -190,6 +117,43 @@ Bind Scope ptype_scope with parametric.base.type.
 Infix "*" := parametric.base.type.prod : ptype_scope.
 Notation "# x" := (parametric.base.type.var_with_subst x) (at level 9, x at level 10, format "# x") : ptype_scope.
 
+Fixpoint upperboundT (t : base.type) : Type
+  := match t with
+     | base.type.nat => option nat
+     | base.type.prod A B => upperboundT A * upperboundT B
+     end.
+
+Module expr.
+  Section with_var.
+    Context {base_type : Type}.
+    Local Notation type := (type base_type).
+    Context {ident : type -> Type}
+            {var : type -> Type}.
+
+    Inductive expr : type -> Type :=
+    | Ident {t} (idc : ident t) : expr t
+    | Var {t} (v : var t) : expr t
+    | Abs {s d} (f : var s -> expr d) : expr (s -> d)
+    | App {s d} (f : expr (s -> d)) (x : expr s) : expr d
+    | LetIn {A B} (x : expr A) (f : var A -> expr B) : expr B
+    .
+  End with_var.
+
+  Module Export Notations.
+    Delimit Scope expr_scope with expr.
+    Bind Scope expr_scope with expr.
+    Infix "@" := App : expr_scope.
+    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 "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : 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.
@@ -204,12 +168,6 @@ Module ident.
     | Pair {A B : base.type} : pident (#A -> #B -> #A * #B)%ptype
     | Fst {A B} : pident (#A * #B -> #A)%ptype
     | Snd {A B} : pident (#A * #B -> #B)%ptype
-    | Nil {A} : pident (parametric.base.type.list #A)%ptype
-    | Cons {A} : pident (#A -> parametric.base.type.list #A -> parametric.base.type.list #A)%ptype
-    | List_map {A B} : pident ((#A -> #B) -> parametric.base.type.list #A -> parametric.base.type.list #B)%ptype
-    | List_app {A} : pident (parametric.base.type.list #A -> parametric.base.type.list #A -> parametric.base.type.list #A)%ptype
-    | List_flat_map {A B} : pident ((#A -> parametric.base.type.list #B) -> parametric.base.type.list #A -> parametric.base.type.list #B)%ptype
-    | List_rect {A P} : pident (#P -> (#A -> parametric.base.type.list #A -> #P -> #P) -> parametric.base.type.list #A -> #P)%ptype
     | Cast {T} (upper_bound : upperboundT T) : pident (#T -> #T)%ptype
     .
 
@@ -231,12 +189,6 @@ Module ident.
     Notation "# x" := (expr.Ident (wrap x)) (at level 9, x at level 10, format "# x") : expr_scope.
     Notation "( x , y , .. , z )" := (expr.App (expr.App (#Pair) .. (expr.App (expr.App (#Pair) x%expr) y%expr) .. ) z%expr) : expr_scope.
     Notation "x + y" := (#Plus @ x @ y)%expr : expr_scope.
-    (*Notation "x :: y" := (#Cons @ x @ y)%expr : expr_scope.*)
-    (* Unification fails if we don't fill in [wident pident] explicitly *)
-    Notation "x :: y" := (@expr.App base.type.type (wident pident) _ _ _ (#Cons @ x) y)%expr : expr_scope.
-    Notation "[ ]" := (#Nil)%expr : expr_scope.
-    Notation "[ x ]" := (#Cons @ x @ (#Nil))%expr : expr_scope.
-    Notation "[ x ; y ; .. ; z ]" :=  (@expr.App base.type.type (wident pident) _ _ _ (#Cons @ x) (#Cons @ y @ .. (#Cons @ z @ #Nil) ..))%expr : expr_scope.
   End Notations.
 End ident.
 Import ident.Notations.
@@ -244,6 +196,37 @@ Notation ident := ident.ident.
 Notation pident := ident.pident.
 Notation wident := ident.wident.
 
+Module UnderLets.
+  Section with_var.
+    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 A) (f : var A -> UnderLets).
+
+    Fixpoint splice {A B} (x : @UnderLets A) (e : A -> @UnderLets B) : @UnderLets B
+      := match x with
+         | Base v => e v
+         | UnderLet A x f => UnderLet x (fun v => @splice _ _ (f v) e)
+         end.
+
+    Fixpoint to_expr {t} (x : @UnderLets (expr t)) : expr t
+      := match x with
+         | Base v => v
+         | UnderLet A x f
+           => expr.LetIn x (fun v => @to_expr _ (f v))
+         end.
+  End with_var.
+  Global Arguments UnderLets : clear implicits.
+End UnderLets.
+Delimit Scope under_lets_scope with under_lets.
+Bind Scope under_lets_scope with UnderLets.UnderLets.
+Notation "x <-- y ; f" := (UnderLets.splice y (fun x => f%under_lets)) : under_lets_scope.
+
 Module partial.
   Import UnderLets.
   Section with_var.
@@ -368,10 +351,6 @@ Module partial.
       Context {var : type -> Type}
               (pident : ptype -> Type).
       Local Notation ident := (wident pident).
-      Context (ident_transport : forall t (P : ident t -> Type) (idc idc' : ident t),
-                  P idc -> option (P idc')).
-      Definition type_transport (P : type -> Type) t t' : P t -> option (P t').
-      Admitted.
       Local Notation expr := (@expr base.type ident).
       Local Notation UnderLets := (@UnderLets base.type ident var).
       Context (abstract_domain' : base.type -> Type).
@@ -393,118 +372,8 @@ Module partial.
               barrier in both directions a decent amount *)
               (ident_Literal : nat -> pident parametric.base.type.nat)
               (ident_Pair : forall A B, pident (#A -> #B -> #A * #B)%ptype)
-              (ident_Nil : forall A, pident (parametric.base.type.list #A)%ptype)
-              (ident_Cons : forall A, pident (#A -> parametric.base.type.list #A -> parametric.base.type.list #A)%ptype)
               (ident_Fst : forall A B, pident (#A * #B -> #A)%ptype)
-              (ident_Snd : forall A B, pident (#A * #B -> #B)%ptype)
-              (hd_tl_list_state : forall A, abstract_domain' (base.type.list A) -> abstract_domain' A * abstract_domain' (base.type.list A)).
-
-
-
-      Inductive base_value : type -> Type :=
-      | Ident {t} (idc : ident t) : base_value t
-      | App {s d} (f : base_value (s -> d)) (x : base_value s) : base_value d
-      | Abs {s d} (f : @expr var (s -> d)) : base_value (s -> d).
-
-      (*(intersect_state : forall A, abstract_domain' A -> abstract_domain' A -> abstract_domain' A)*)
-
-
-      Local Notation value := (@value base.type ident var base_value abstract_domain').
-
-      Definition abstraction_function : forall t : base.type, base_value t -> abstract_domain' t
-        := fun _ _ => bottom' _.
-
-      Fixpoint base_reify {t} (e : base_value t) : @expr var t
-        := match e in base_value t return expr t with
-           | Ident t idc => ###idc
-           | App s d f x => @base_reify _ f @ (@base_reify _ x)
-           | Abs s d f => f
-           end%expr.
-
-      Local Notation reflect := (@reflect base.type ident var base_value abstract_domain' annotate bottom' (@abstraction_function) (@base_reify)).
-      Local Notation bottom := (@bottom base.type abstract_domain' bottom').
-
-      Fixpoint base_reflect {t} : base_value t -> value t
-        := match t return base_value t -> value t with
-           | type.base t => @inr _ _
-           | type.arrow s d => fun v => reflect (base_reify v) bottom
-           end.
-
-      Inductive pattern : type -> Type :=
-      | PIdent {t} (idc : ident t) : pattern t
-      | PApp {s d} (f : pattern (s -> d)) (x : pattern s) : pattern d
-      | PVar {t} : pattern t.
-
-      Fixpoint pattern_bound {t} (p : pattern t) : Type
-        := match p with
-           | PIdent t idc => unit
-           | PApp s d f x => @pattern_bound _ f * @pattern_bound _ x
-           | PVar t => value t
-           end.
-
-      Fixpoint pattern_matches {t} (p : pattern t) (v : base_value t) : option (pattern_bound p).
-        refine match p, v return option (pattern_bound p) with
-               | PIdent t idc, Ident t' idc'
-                 => (idc'' <- type_transport ident _ _ idc';
-                     ident_transport _ (fun _ => unit) idc idc'' tt)
-               | PApp s d f x, App s' d' f' x'
-                 => (f'' <- type_transport base_value _ _ f';
-                     x'' <- type_transport base_value _ _ x';
-                     sb <- @pattern_matches _ f f'';
-                     db <- @pattern_matches _ x x'';
-                     Some (sb, db))
-               | PVar t, e
-                 => (e' <- type_transport base_value _ t e;
-                     _)
-               | PIdent _ _, _ => None
-               | PApp _ _ _ _, _ => None
-               end%option.
-        refine match p in pattern t return base_value t -> option (pattern_bound p) with
-               | PIdent t idc
-                 => fun v
-                    => match v in base_value t return ident t -> option unit with
-                       | Ident t idc'
-                         => fun idc => ident_transport _ (fun _ => unit) idc idc' tt
-                       | App _ _ _ _
-                       | Abs _ _ _
-                         => fun _ => None
-                       end idc
-               | PApp s d f x
-                 => fun v
-                    => let v' := match v in base_value d return option (base_value  with
-                                 | Ident t idc => _
-                                 | App s d f x => _
-                                 | Abs s d f => _
-                                 end
-               (*
-                      let f' := fun v' => @pattern_matches _ f v' in
-                       let x' := fun v' => @pattern_matches _ x v' in
-                       _*)
-               | PVar t => _
-               end.
-        cbn.
-
-        Focus 3.
-        cbn.
-
-      Context (do_rewrite_rules
-      Context (half_interp : forall {t} (idc : pident t), parametric.half_interp UnderLets value t).
-
-
-
-
-
-
-      Definition interp_ident : forall t, ident t -> value t.
-                                                                   := match idc in ident.wident _ t return value t with
-           | ident.wrap T idc' as idc
-             => pinterp
-                  (Base (reflect (###idc) (abstract_interp_ident _ idc')))%expr
-                  (half_interp _ idc')
-           end.
-
-
-      (base_reify : forall t, base_value t -> @expr var t).
+              (ident_Snd : forall A B, pident (#A * #B -> #B)%ptype).
 
       Fixpoint base_value (t : base.type)
         := match t return Type with
@@ -512,8 +381,6 @@ Module partial.
              => nat
            | base.type.prod A B as t
              => (abstract_domain' A * @expr var A + base_value A) * (abstract_domain' B * @expr var B + base_value B)
-           | base.type.list A as t
-             => list (abstract_domain' A * @expr var A + base_value A) (* cons cells *) * option (abstract_domain' (base.type.list A) * @expr var (base.type.list A))
            end%type.
 
       Fixpoint abstraction_function {t} : base_value t -> abstract_domain' t
@@ -532,22 +399,6 @@ Module partial.
                               end in
                    abstract_interp_ident
                      _ (ident_Pair A B) sta stb
-           | base.type.list A
-             => fun '(cells, rest)
-                => let st_cells := List.map
-                                     (fun a => match a with
-                                               | inl (st, _) => st
-                                               | inr a' => @abstraction_function A a'
-                                               end)
-                                     cells in
-                   let st_rest := match rest with
-                                  | None => abstract_interp_ident _ (ident_Nil A)
-                                  | Some (st, _) => st
-                                  end in
-                   List.fold_right
-                     (abstract_interp_ident _ (ident_Cons A))
-                     st_rest
-                     st_cells
            end.
 
       Fixpoint base_reify {t} : base_value t -> @expr var t
@@ -573,38 +424,12 @@ Module partial.
                              | inr v => @base_reify _ v
                              end in
                    (#(ident_Pair A B) @ ea @ eb)%expr
-           | base.type.list A
-             => fun '(cons_cells, rest)
-                => let cells' := List.map
-                                   (fun a => match a with
-                                             | inl (st, e)
-                                               => match annotate _ st with
-                                                  | None => e
-                                                  | Some cst => ###cst @ e
-                                                  end%expr
-                                             | inr v => @base_reify _ v
-                                             end)
-                                   cons_cells in
-                   let rest' := match rest with
-                                | Some (st, e)
-                                  => match annotate _ st with
-                                     | None => e
-                                     | Some cst => ###cst @ e
-                                     end%expr
-                                | None => (#(ident_Nil A))%expr
-                                end in
-                   List.fold_right
-                     (fun x xs => (#(ident_Cons A) @ x @ xs)%expr)
-                     rest'
-                     cells'
            end.
 
       Local Notation value := (@value base.type ident var base_value abstract_domain').
 
       Context (half_interp : forall {t} (idc : pident t), parametric.half_interp UnderLets value t).
 
-      Print List.fold_left.
-
       Fixpoint intersect_state_base_value {t} : abstract_domain' t -> base_value t -> base_value t
         := match t return abstract_domain' t -> base_value t -> base_value t with
            | base.type.nat => update_literal_with_state
@@ -621,25 +446,6 @@ Module partial.
                              | inr v => inr (@intersect_state_base_value _ stb v)
                              end in
                    (a', b')
-           | base.type.list _
-             => fun st '(cons_cells, rest)
-                => let '(cells', st_rest)
-                       := List.fold_left
-                            (fun '(rest_cells, st) cell
-                             => let '(st0, st') := hd_tl_list_state _ st in
-                                (match cell with
-                                 | inl (st0', e) => inl (intersect_state _ st0 st0', e)
-                                 | inr v => inr (@intersect_state_base_value _ st0 v)
-                                 end :: rest_cells,
-                                 st'))
-                            cons_cells
-                            (nil, st) in
-                   (cells',
-                    match rest with
-                    | None => None
-                    | Some (st_rest', e)
-                      => Some (intersect_state _ st_rest st_rest', e)
-                    end)
            end.
 
 
@@ -664,14 +470,12 @@ Module partial.
              => fun v => inr v
            | parametric.base.type.prod A B
              => fun '(a, b) => inr (@pinterp_base A a, @pinterp_base B b)
-           | parametric.base.type.list A
-             => fun ls => inr (List.map (@pinterp_base A) ls, None)
            | parametric.base.type.var_with_subst subst
              => fun v => v
            end.
 
-      Fixpoint puninterp_base {t : parametric.base.type} : value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t)).
-          refine match t return value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t)) with
+      Fixpoint puninterp_base {t : parametric.base.type} : value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t))
+        := match t return value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t)) with
            | parametric.base.type.nat
              => fun v
                 => match v with
@@ -687,19 +491,9 @@ Module partial.
                            b' <- @puninterp_base B b;
                            Some (a', b'))
                    end
-           | parametric.base.type.list A
-             => fun ls
-                => match ls with
-                   | inl _ => None
-                   | inr (cons_cells, rest)
-                     => _
-                   end
            | parametric.base.type.var_with_subst subst
              => @Some _
-                 end%option.
-          fold parametric.base.type.subst in *.
-          fold base_value in *.
-          cbn in *.
+           end%option.
 
       (* FIXME: naming; these are basically just fancy identity functions *)
       Fixpoint vinterp_arrow {t : type} : value t -> @type.interpM base.type UnderLets value t