Merge pull request #1774 from JasonGross/saturated-solinas-idents-more

Add remaining identifiers for saturated solinas
mit-plv · Dec 8, 2023 · 7c7c435 · 7c7c435
2 parents 0c66069 + 02afb84
commit 7c7c435
Show file tree

Hide file tree

Showing 7 changed files with 172 additions and 236 deletions.
diff --git a/src/AbstractInterpretation/ZRange.v b/src/AbstractInterpretation/ZRange.v
@@ -681,10 +681,8 @@ Module Compilers.
                    end
              | ident.nat_rect_arrow _ _ as idc
              | ident.eager_nat_rect_arrow _ _ as idc
-               (*
              | ident.nat_rect_fbb_b _ _ _ as idc
              | ident.nat_rect_fbb_b_b _ _ _ _ as idc
-                *)
                => fun O_case S_case n
                   => let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in
                    match n return type.option.interp t with
@@ -710,13 +708,11 @@ Module Compilers.
                    end
              | ident.list_rect_arrow _ _ _ as idc
              | ident.eager_list_rect_arrow _ _ _ as idc
-               (*
              | ident.list_rect_fbb_b _ _ _ _ as idc
              | ident.list_rect_fbb_b_b _ _ _ _ _ as idc
              | ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc
              | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc
              | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ as idc
-                *)
                => fun N C ls
                  => let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in
                    match ls return type.option.interp t with

diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v
diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
@@ -1187,15 +1187,13 @@ Proof.
           | ident.eager_list_rect _ _
           | ident.list_rect_arrow _ _ _
           | ident.eager_list_rect_arrow _ _ _
-          (*
           | ident.nat_rect_fbb_b _ _ _
           | ident.nat_rect_fbb_b_b _ _ _ _
           | ident.list_rect_fbb_b _ _ _ _
           | ident.list_rect_fbb_b_b _ _ _ _ _
           | ident.list_rect_fbb_b_b_b _ _ _ _ _ _
           | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _
           | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _
-           *)
           | ident.list_case _ _
           | ident.List_map _ _
           | ident.List_flat_map _ _

diff --git a/src/Language/APINotations.v b/src/Language/APINotations.v
@@ -81,21 +81,17 @@ Module Compilers.
   Global Arguments ident_nat_rect_arrow {_ _} : assert.
   Global Arguments ident_eager_nat_rect {_} : assert.
   Global Arguments ident_eager_nat_rect_arrow {_ _} : assert.
-  (*
   Global Arguments ident_nat_rect_fbb_b {_ _ _} : assert.
   Global Arguments ident_nat_rect_fbb_b_b {_ _ _ _} : assert.
-*)
   Global Arguments ident_list_rect {_ _} : assert.
   Global Arguments ident_eager_list_rect {_ _} : assert.
   Global Arguments ident_eager_list_rect_arrow {_ _ _} : assert.
   Global Arguments ident_list_rect_arrow {_ _ _} : assert.
-  (*
   Global Arguments ident_list_rect_fbb_b {_ _ _ _} : assert.
   Global Arguments ident_list_rect_fbb_b_b {_ _ _ _ _} : assert.
   Global Arguments ident_list_rect_fbb_b_b_b {_ _ _ _ _ _} : assert.
   Global Arguments ident_list_rect_fbb_b_b_b_b {_ _ _ _ _ _ _} : assert.
   Global Arguments ident_list_rect_fbb_b_b_b_b_b {_ _ _ _ _ _ _ _} : assert.
-*)
   Global Arguments ident_list_case {_ _} : assert.
   Global Arguments ident_List_length {_} : assert.
   Global Arguments ident_List_firstn {_} : assert.
@@ -257,21 +253,17 @@ Module Compilers.
     Notation nat_rect_arrow := Compilers.ident_nat_rect_arrow (only parsing).
     Notation eager_nat_rect := Compilers.ident_eager_nat_rect (only parsing).
     Notation eager_nat_rect_arrow := Compilers.ident_eager_nat_rect_arrow (only parsing).
-    (*
     Notation nat_rect_fbb_b := Compilers.ident_nat_rect_fbb_b (only parsing).
     Notation nat_rect_fbb_b_b := Compilers.ident_nat_rect_fbb_b_b (only parsing).
-*)
     Notation list_rect := Compilers.ident_list_rect (only parsing).
     Notation list_rect_arrow := Compilers.ident_list_rect_arrow (only parsing).
     Notation eager_list_rect := Compilers.ident_eager_list_rect (only parsing).
     Notation eager_list_rect_arrow := Compilers.ident_eager_list_rect_arrow (only parsing).
-    (*
     Notation list_rect_fbb_b := Compilers.ident_list_rect_fbb_b (only parsing).
     Notation list_rect_fbb_b_b := Compilers.ident_list_rect_fbb_b_b (only parsing).
     Notation list_rect_fbb_b_b_b := Compilers.ident_list_rect_fbb_b_b_b (only parsing).
     Notation list_rect_fbb_b_b_b_b := Compilers.ident_list_rect_fbb_b_b_b_b (only parsing).
     Notation list_rect_fbb_b_b_b_b_b := Compilers.ident_list_rect_fbb_b_b_b_b_b (only parsing).
-*)
     Notation list_case := Compilers.ident_list_case (only parsing).
     Notation List_length := Compilers.ident_List_length (only parsing).
     Notation List_seq := Compilers.ident_List_seq (only parsing).

diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v
@@ -111,21 +111,17 @@ Definition all_ident_named_interped : InductiveHList.hlist
       ; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect))
       ; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep)
       ; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep))
-                  (*
       ; with_name ident_nat_rect_fbb_b (@nat_rect_fbb_b)
       ; with_name ident_nat_rect_fbb_b_b (@nat_rect_fbb_b_b)
-*)
       ; with_name ident_list_rect (@Thunked.list_rect)
       ; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect))
       ; with_name ident_list_rect_arrow (@list_rect_arrow_nodep)
       ; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep))
-                  (*
       ; with_name ident_list_rect_fbb_b (@list_rect_fbb_b)
       ; with_name ident_list_rect_fbb_b_b (@list_rect_fbb_b_b)
       ; with_name ident_list_rect_fbb_b_b_b (@list_rect_fbb_b_b_b)
       ; with_name ident_list_rect_fbb_b_b_b_b (@list_rect_fbb_b_b_b_b)
       ; with_name ident_list_rect_fbb_b_b_b_b_b (@list_rect_fbb_b_b_b_b_b)
-*)
       ; with_name ident_list_case (@Thunked.list_case)
       ; with_name ident_List_length (@List.length)
       ; with_name ident_List_seq (@List.seq)

diff --git a/src/Stringification/IR.v b/src/Stringification/IR.v
@@ -809,15 +809,13 @@ Module Compilers.
                  | ident.eager_list_rect _ _
                  | ident.list_rect_arrow _ _ _
                  | ident.eager_list_rect_arrow _ _ _
-                 (*
                  | ident.nat_rect_fbb_b _ _ _
                  | ident.nat_rect_fbb_b_b _ _ _ _
                  | ident.list_rect_fbb_b _ _ _ _
                  | ident.list_rect_fbb_b_b _ _ _ _ _
                  | ident.list_rect_fbb_b_b_b _ _ _ _ _ _
                  | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _
                  | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _
-                  *)
                  | ident.list_case _ _
                  | ident.List_length _
                  | ident.List_seq

diff --git a/src/Stringification/Language.v b/src/Stringification/Language.v
@@ -411,15 +411,13 @@ Module Compilers.
                 | ident.eager_nat_rect P => neg_wrap_parens "eager_nat_rect"
                 | ident.nat_rect_arrow P Q => neg_wrap_parens "nat_rect(→)"
                 | ident.eager_nat_rect_arrow P Q => neg_wrap_parens "eager_nat_rect(→)"
-                (*
                 | @ident.nat_rect_fbb_b A B C => neg_wrap_parens "nat_rect_fbb_b"
                 | @ident.nat_rect_fbb_b_b A B C D => neg_wrap_parens "nat_rect_fbb_b_b"
                 | @ident.list_rect_fbb_b T A B C => neg_wrap_parens "list_rect_fbb_b"
                 | @ident.list_rect_fbb_b_b T A B C D => neg_wrap_parens "list_rect_fbb_b_b"
                 | @ident.list_rect_fbb_b_b_b T A B C D E => neg_wrap_parens "list_rect_fbb_b_b"
                 | @ident.list_rect_fbb_b_b_b_b T A B C D E F => neg_wrap_parens "list_rect_fbb_b_b"
                 | @ident.list_rect_fbb_b_b_b_b_b T A B C D E F G => neg_wrap_parens "list_rect_fbb_b_b"
-                 *)
                 | ident.list_rect A P => neg_wrap_parens "list_rect"
                 | ident.eager_list_rect A P => neg_wrap_parens "eager_list_rect"
                 | ident.list_rect_arrow A P Q => neg_wrap_parens "list_rect(→)"
@@ -706,15 +704,13 @@ Module Compilers.
              | ident.eager_nat_rect _ as idc
              | ident.eager_nat_rect_arrow _ _ as idc
              | ident.nat_rect_arrow _ _ as idc
-             (*
              | @ident.nat_rect_fbb_b    _ _ _ as idc
              | @ident.nat_rect_fbb_b_b  _ _ _ _ as idc
              | @ident.list_rect_fbb_b   _ _ _ _ as idc
              | @ident.list_rect_fbb_b_b _ _ _ _ _ as idc
              | @ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc
              | @ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc
              | @ident.list_rect_fbb_b_b_b_b_b  _ _ _ _ _ _ _ _ as idc
-              *)
              | ident.option_rect _ _ as idc
              | ident.list_rect _ _ as idc
              | ident.eager_list_rect _ _ as idc