From a714d4b1cc90089b80ac475f5b6882f05e98c355 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 25 Jan 2019 16:36:25 -0500
Subject: Support Nat.eqb in reification

---
 src/AbstractInterpretation.v           |  1 +
 src/CStringification.v                 |  3 +++
 src/GENERATEDIdentifiersWithoutTypes.v | 23 +++++++++++++++++++++++
 src/Language.v                         |  2 ++
 src/arith_rewrite_head.out             |  1 +
 src/arith_with_casts_rewrite_head.out  |  1 +
 src/fancy_rewrite_head.out             |  1 +
 src/fancy_with_casts_rewrite_head.out  |  1 +
 src/nbe_rewrite_head.out               | 33 +++++++++++++++++++++++++++++++++
 9 files changed, 66 insertions(+)

diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 463cc72cd..4d82b869a 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -377,6 +377,7 @@ Module Compilers.
              | ident.Nat_mul as idc
              | ident.Nat_add as idc
              | ident.Nat_sub as idc
+             | ident.Nat_eqb as idc
              | ident.List_seq as idc
                => fun x y => x <- x; y <- y; rSome (ident.interp idc x y)
              | ident.List_repeat _
diff --git a/src/CStringification.v b/src/CStringification.v
index 6aba9746f..5c73b8e26 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -211,6 +211,7 @@ Module Compilers.
              | ident.Nat_mul => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " *ℕ " ++ y 39%nat), ZRange.type.base.option.None)
              | ident.Nat_add => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " +ℕ " ++ y 49%nat), ZRange.type.base.option.None)
              | ident.Nat_sub => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " -ℕ " ++ y 49%nat), ZRange.type.base.option.None)
+             | ident.Nat_eqb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " =ℕ " ++ y 69%nat), ZRange.type.base.option.None)
              | ident.nil t => fun 'tt => (fun _ => "[]", ZRange.type.base.option.None)
              | ident.cons t => fun '(x, ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 60) (maybe_wrap_cast with_casts x 59%nat ++ " :: " ++ y 60%nat), ZRange.type.base.option.None)
              | ident.pair A B => fun '(x, (y, tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 201) (maybe_wrap_cast with_casts x 201%nat ++ ", " ++ maybe_wrap_cast with_casts y 200%nat), ZRange.type.base.option.None)
@@ -340,6 +341,7 @@ Module Compilers.
                 | ident.Nat_mul => "Nat.mul"
                 | ident.Nat_add => "Nat.add"
                 | ident.Nat_sub => "Nat.sub"
+                | ident.Nat_eqb => "Nat.eqb"
                 | ident.nil t => "[]"
                 | ident.cons t => "(::)"
                 | ident.pair A B => "(,)"
@@ -1175,6 +1177,7 @@ Module Compilers.
                | ident.Nat_mul
                | ident.Nat_add
                | ident.Nat_sub
+               | ident.Nat_eqb
                | ident.prod_rect _ _ _
                | ident.bool_rect _
                | ident.nat_rect _
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index a682df8a2..a5e96870f 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -156,6 +156,13 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                    (Compilers.base.type.type_base base.type.nat) ->
                  (fun x : Compilers.base.type => type.base x)
                    (Compilers.base.type.type_base base.type.nat))%ptype
+  | Nat_eqb : ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.bool))%ptype
   | nil : forall t : Compilers.base.type,
           ident
             ((fun x : Compilers.base.type => type.base x)
@@ -711,6 +718,7 @@ show_match_ident = r"""match # with
  | ident.Nat_mul =>
  | ident.Nat_add =>
  | ident.Nat_sub =>
+ | ident.Nat_eqb =>
  | ident.nil t =>
  | ident.cons t =>
  | ident.pair A B =>
@@ -1281,6 +1289,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
         | Nat_mul
         | Nat_add
         | Nat_sub
+        | Nat_eqb
         | nil
         | cons
         | pair
@@ -1361,6 +1370,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Nat_mul => unit
              | Nat_add => unit
              | Nat_sub => unit
+             | Nat_eqb => unit
              | nil => Compilers.base.type
              | cons => Compilers.base.type
              | pair => Compilers.base.type * Compilers.base.type
@@ -1442,6 +1452,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Nat_mul => true
              | Nat_add => true
              | Nat_sub => true
+             | Nat_eqb => true
              | nil => false
              | cons => false
              | pair => false
@@ -1523,6 +1534,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Nat_mul, Compilers.ident.Nat_mul => Some tt
              | Nat_add, Compilers.ident.Nat_add => Some tt
              | Nat_sub, Compilers.ident.Nat_sub => Some tt
+             | Nat_eqb, Compilers.ident.Nat_eqb => Some tt
              | nil, Compilers.ident.nil t => Some t
              | cons, Compilers.ident.cons t => Some t
              | pair, Compilers.ident.pair A B => Some (A, B)
@@ -1600,6 +1612,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Nat_mul, _
              | Nat_add, _
              | Nat_sub, _
+             | Nat_eqb, _
              | nil, _
              | cons, _
              | pair, _
@@ -1682,6 +1695,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Nat_mul => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
              | Nat_add => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
              | Nat_sub => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Nat_eqb => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
              | nil => fun t => (type.base (Compilers.base.type.list t))
              | cons => fun t => (type.base t -> type.base (Compilers.base.type.list t) -> type.base (Compilers.base.type.list t))%ptype
              | pair => fun arg => let '(A, B) := eta2 arg in (type.base A -> type.base B -> type.base (A * B)%etype)%ptype
@@ -1763,6 +1777,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Nat_mul => fun _ => @Compilers.ident.Nat_mul
              | Nat_add => fun _ => @Compilers.ident.Nat_add
              | Nat_sub => fun _ => @Compilers.ident.Nat_sub
+             | Nat_eqb => fun _ => @Compilers.ident.Nat_eqb
              | nil => fun t => @Compilers.ident.nil t
              | cons => fun t => @Compilers.ident.cons t
              | pair => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of pair arg') with (A, B) => @Compilers.ident.pair A B end
@@ -1851,6 +1866,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.Nat_mul => f _ Compilers.ident.Nat_mul
            | Compilers.ident.Nat_add => f _ Compilers.ident.Nat_add
            | Compilers.ident.Nat_sub => f _ Compilers.ident.Nat_sub
+           | Compilers.ident.Nat_eqb => f _ Compilers.ident.Nat_eqb
            | Compilers.ident.nil t => f _ (@Compilers.ident.nil t)
            | Compilers.ident.cons t => f _ (@Compilers.ident.cons t)
            | Compilers.ident.pair A B => f _ (@Compilers.ident.pair A B)
@@ -1931,6 +1947,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
       | Nat_mul : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
       | Nat_add : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
       | Nat_sub : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Nat_eqb : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.bool))%ptype
       | nil {t : base.type} : ident (type.base (base.type.list t))
       | cons {t : base.type} : ident (type.base t -> type.base (base.type.list t) -> type.base (base.type.list t))%ptype
       | pair {A : base.type} {B : base.type} : ident (type.base A -> type.base B -> type.base (A * B)%pbtype)%ptype
@@ -2011,6 +2028,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Nat_mul => Raw.ident.Nat_mul
            | @Nat_add => Raw.ident.Nat_add
            | @Nat_sub => Raw.ident.Nat_sub
+           | @Nat_eqb => Raw.ident.Nat_eqb
            | @nil t => Raw.ident.nil
            | @cons t => Raw.ident.cons
            | @pair A B => Raw.ident.pair
@@ -2092,6 +2110,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Nat_mul => []
            | @Nat_add => []
            | @Nat_sub => []
+           | @Nat_eqb => []
            | @nil t => []
            | @cons t => []
            | @pair A B => []
@@ -2173,6 +2192,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Nat_mul => fun _ => @Compilers.ident.Nat_mul
            | @Nat_add => fun _ => @Compilers.ident.Nat_add
            | @Nat_sub => fun _ => @Compilers.ident.Nat_sub
+           | @Nat_eqb => fun _ => @Compilers.ident.Nat_eqb
            | @nil t => fun _ => @Compilers.ident.nil _
            | @cons t => fun _ => @Compilers.ident.cons _
            | @pair A B => fun _ => @Compilers.ident.pair _ _
@@ -2257,6 +2277,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Nat_mul, Compilers.ident.Nat_mul => Some tt
            | @Nat_add, Compilers.ident.Nat_add => Some tt
            | @Nat_sub, Compilers.ident.Nat_sub => Some tt
+           | @Nat_eqb, Compilers.ident.Nat_eqb => Some tt
            | @nil t, Compilers.ident.nil t' => Some tt
            | @cons t, Compilers.ident.cons t' => Some tt
            | @pair A B, Compilers.ident.pair A' B' => Some tt
@@ -2334,6 +2355,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Nat_mul, _
            | @Nat_add, _
            | @Nat_sub, _
+           | @Nat_eqb, _
            | @nil _, _
            | @cons _, _
            | @pair _ _, _
@@ -2416,6 +2438,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.Nat_mul => @Nat_mul
            | Compilers.ident.Nat_add => @Nat_add
            | Compilers.ident.Nat_sub => @Nat_sub
+           | Compilers.ident.Nat_eqb => @Nat_eqb
            | Compilers.ident.nil t => @nil (base.relax t)
            | Compilers.ident.cons t => @cons (base.relax t)
            | Compilers.ident.pair A B => @pair (base.relax A) (base.relax B)
diff --git a/src/Language.v b/src/Language.v
index eba5cf85a..e4c5057db 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -855,6 +855,7 @@ Module Compilers.
         | Nat_mul : ident (nat -> nat -> nat)
         | Nat_add : ident (nat -> nat -> nat)
         | Nat_sub : ident (nat -> nat -> nat)
+        | Nat_eqb : ident (nat -> nat -> bool)
         | nil {t} : ident (list t)
         | cons {t:base.type} : ident (t -> list t -> list t)
         | pair {A B:base.type} : ident (A -> B -> A * B)
@@ -995,6 +996,7 @@ Module Compilers.
              | Nat_mul => Nat.mul
              | Nat_add => Nat.add
              | Nat_sub => Nat.sub
+             | Nat_eqb => Nat.eqb
              | nil t => Datatypes.nil
              | cons t => Datatypes.cons
              | pair A B => Datatypes.pair
diff --git a/src/arith_rewrite_head.out b/src/arith_rewrite_head.out
index 4a3eb8e80..669f6f8c8 100644
--- a/src/arith_rewrite_head.out
+++ b/src/arith_rewrite_head.out
@@ -7,6 +7,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
 | Nat_mul => fun x x0 : expr ℕ => Base (#(Nat_mul)%expr @ x @ x0)%expr_pat
 | Nat_add => fun x x0 : expr ℕ => Base (#(Nat_add)%expr @ x @ x0)%expr_pat
 | Nat_sub => fun x x0 : expr ℕ => Base (#(Nat_sub)%expr @ x @ x0)%expr_pat
+| Nat_eqb => fun x x0 : expr ℕ => Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat
 | @nil t => Base []%expr_pat
 | @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
 | @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out
index a179fff11..e85d57fd0 100644
--- a/src/arith_with_casts_rewrite_head.out
+++ b/src/arith_with_casts_rewrite_head.out
@@ -7,6 +7,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
 | Nat_mul => fun x x0 : expr ℕ => Base (#(Nat_mul)%expr @ x @ x0)%expr_pat
 | Nat_add => fun x x0 : expr ℕ => Base (#(Nat_add)%expr @ x @ x0)%expr_pat
 | Nat_sub => fun x x0 : expr ℕ => Base (#(Nat_sub)%expr @ x @ x0)%expr_pat
+| Nat_eqb => fun x x0 : expr ℕ => Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat
 | @nil t => Base []%expr_pat
 | @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
 | @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
diff --git a/src/fancy_rewrite_head.out b/src/fancy_rewrite_head.out
index 414237570..1e672a07e 100644
--- a/src/fancy_rewrite_head.out
+++ b/src/fancy_rewrite_head.out
@@ -7,6 +7,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
 | Nat_mul => fun x x0 : expr ℕ => Base (#(Nat_mul)%expr @ x @ x0)%expr_pat
 | Nat_add => fun x x0 : expr ℕ => Base (#(Nat_add)%expr @ x @ x0)%expr_pat
 | Nat_sub => fun x x0 : expr ℕ => Base (#(Nat_sub)%expr @ x @ x0)%expr_pat
+| Nat_eqb => fun x x0 : expr ℕ => Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat
 | @nil t => Base []%expr_pat
 | @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
 | @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
diff --git a/src/fancy_with_casts_rewrite_head.out b/src/fancy_with_casts_rewrite_head.out
index c35ff8a01..4a5354593 100644
--- a/src/fancy_with_casts_rewrite_head.out
+++ b/src/fancy_with_casts_rewrite_head.out
@@ -7,6 +7,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
 | Nat_mul => fun x x0 : expr ℕ => Base (#(Nat_mul)%expr @ x @ x0)%expr_pat
 | Nat_add => fun x x0 : expr ℕ => Base (#(Nat_add)%expr @ x @ x0)%expr_pat
 | Nat_sub => fun x x0 : expr ℕ => Base (#(Nat_sub)%expr @ x @ x0)%expr_pat
+| Nat_eqb => fun x x0 : expr ℕ => Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat
 | @nil t => Base []%expr_pat
 | @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
 | @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
diff --git a/src/nbe_rewrite_head.out b/src/nbe_rewrite_head.out
index cbd282f50..bf9101f5e 100644
--- a/src/nbe_rewrite_head.out
+++ b/src/nbe_rewrite_head.out
@@ -175,6 +175,39 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
       end;;
       None);;;
      Base (#(Nat_sub)%expr @ x @ x0)%expr_pat)%option
+| Nat_eqb =>
+    fun x x0 : expr ℕ =>
+    ((match x with
+      | @expr.Ident _ _ _ t idc =>
+          match x0 with
+          | @expr.Ident _ _ _ t0 idc0 =>
+              args <- invert_bind_args idc0 Raw.ident.Literal;
+              args0 <- invert_bind_args idc Raw.ident.Literal;
+              match
+                pattern.type.unify_extracted_cps (ℕ -> ℕ)%ptype
+                  ((projT1 args0) -> (projT1 args))%ptype option
+                  (fun x1 : option => x1)
+              with
+              | Some (_, _)%zrange =>
+                  if
+                   type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype
+                     ((projT1 args0) -> (projT1 args))%ptype
+                  then
+                   xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
+                   xv0 <- ident.unify pattern.ident.Literal ##(projT2 args);
+                   Some
+                     (Base
+                        (##((let (x1, _) := xv in x1) =?
+                            (let (x1, _) := xv0 in x1))%nat)%expr)
+                  else None
+              | None => None
+              end
+          | _ => None
+          end
+      | _ => None
+      end;;
+      None);;;
+     Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat)%option
 | @nil t => Base []%expr_pat
 | @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
 | @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
-- 
cgit v1.2.3