From fc67c2ddd3766cfbc07a8bfb7d7ae96c7cf36545 Mon Sep 17 00:00:00 2001
From: Leonidas Lampropoulos <lemonidas_13@hotmail.com>
Date: Fri, 21 Jun 2024 09:28:48 -0400
Subject: [PATCH] Fix totality checker in match_inp to correctly account for
 inductive type parameters (#381)

---
 examples/other/DependentTest.v | 67 ++++++++++++++++++++++++++++++++++
 plugin/arbitrarySizedST.ml     |  6 ++-
 plugin/genericLib.ml.cppo      |  5 +++
 plugin/genericLib.mli          |  1 +
 4 files changed, 77 insertions(+), 2 deletions(-)

diff --git a/examples/other/DependentTest.v b/examples/other/DependentTest.v
index e7bd93b31..e2cade745 100644
--- a/examples/other/DependentTest.v
+++ b/examples/other/DependentTest.v
@@ -432,5 +432,72 @@ Inductive goodFun : Foo -> Prop :=
 
 Derive ArbitrarySizedSuchThat for (fun a => goodFun a).
 
+Inductive Foo_and : (bool * bool) -> bool -> Prop :=
+  | Foo_andtt : Foo_and (true, true) true.
+
+Inductive Foo_rel : nat -> bool -> Prop :=
+  | R1 : forall n,
+       Foo_rel n true
+  | R2' : forall a1 l1 a2 l2 l,
+       Foo_and (l1, l2) l ->
+       Foo_rel a1 l1 ->
+       Foo_rel a2 l2 ->
+       Foo_rel a1 l.
+
+Derive Generator for (fun l12 => Foo_and l12 l).
+Derive Generator for (fun a => Foo_rel a b).
+
+Definition gen_foo_and (l : bool) : nat -> G (option (bool * bool)) :=
+    let
+      fix aux_arb (init_size size : nat) (l_0 : bool) {struct size} : G (option (bool * bool)) :=
+        match size with
+        | 0 | _ =>
+            backtrack
+              [(1,
+                thunkGen
+                  (fun _ : unit => if l_0 then returnGen (Some (true, true)) else returnGen None))]
+        end in
+    fun size : nat => aux_arb size size l.
+
+Lemma gen_foo_and_equality l : 
+  gen_foo_and l = @arbitrarySizeST _ (fun l12 => Foo_and l12 l) _. 
+Proof. reflexivity. Qed. 
+
+Definition gen_foo_rel (b_ : bool) : nat -> G (option nat) :=
+    let
+      fix aux_arb (init_size size : nat) (b_0 : bool) {struct size} : G (option nat) :=
+        match size with
+        | 0 =>
+            backtrack
+              [(1,
+                thunkGen
+                  (fun _ : unit =>
+                   if b_0
+                   then bindGen arbitrary (fun n : nat => returnGen (Some n))
+                   else returnGen None)); (1, thunkGen (fun _ : unit => returnGen None))]
+        | S size' =>
+            backtrack
+              [(1,
+                thunkGen
+                  (fun _ : unit =>
+                   if b_0
+                   then bindGen arbitrary (fun n : nat => returnGen (Some n))
+                   else returnGen None));
+               (S size',
+                thunkGen
+                  (fun _ : unit =>
+                   bindOpt (genST (fun unkn_11_ : bool * bool => Foo_and unkn_11_ b_0))
+                     (fun unkn_11_ : bool * bool =>
+                      let (l1, l2) := unkn_11_ in
+                      bindOpt (aux_arb init_size size' l1)
+                        (fun a_ : nat =>
+                         bindOpt (aux_arb init_size size' l2) (fun _ : nat => returnGen (Some a_))))))]
+        end in
+    fun size : nat => aux_arb size size b_.
+
+Lemma gen_foo_rel_equality b : 
+  gen_foo_rel b = @arbitrarySizeST _ (fun l => Foo_rel l b) _. 
+Proof. reflexivity. Qed. 
+
 Definition success := "success".
 Print success.
diff --git a/plugin/arbitrarySizedST.ml b/plugin/arbitrarySizedST.ml
index 06f8baf9b..2ecae1751 100644
--- a/plugin/arbitrarySizedST.ml
+++ b/plugin/arbitrarySizedST.ml
@@ -70,14 +70,16 @@ let check_expr (n : int) (scrut : coq_expr) (left : coq_expr) (right : coq_expr)
     ]
 
 let match_inp (inp : var) (pat : matcher_pat) (left : coq_expr) (right  : coq_expr) =
+  msg_debug (str (Printf.sprintf "Calling match inp with %s %s\n" (var_to_string inp) (matcher_pat_to_string pat)) ++ fnl ());
   let ret v left right =
     construct_match (gVar v) ~catch_all:(Some right) [(pat, left)]
   in
   let catch_case = 
     match pat with 
-    | MatchCtr (c, ls) -> 
+    | MatchCtr (c, ls) ->
+       msg_debug (str (Printf.sprintf "In catch case: %s : %s\n" (matcher_pat_to_string pat) (string_of_int (num_of_ctrs c))) ++ fnl ());
        (* Leo: This is a hack totality check for unary matches *)
-       if num_of_ctrs c = 1 && List.for_all (fun x -> match x with MatchU _ -> true | MatchCtr _ -> false) ls 
+       if num_of_ctrs c = 1 && List.for_all (fun x -> match x with MatchU _ -> true | MatchParameter _ -> true | MatchCtr (c',_) -> belongs_to_inductive c') ls 
        then None
        else Some right
     | _ -> failwith "Toplevel match not a constructor?"
diff --git a/plugin/genericLib.ml.cppo b/plugin/genericLib.ml.cppo
index 9dd19a34b..70ff10149 100644
--- a/plugin/genericLib.ml.cppo
+++ b/plugin/genericLib.ml.cppo
@@ -162,6 +162,11 @@ let num_of_ctrs (c : constructor) =
   let mib = Environ.lookup_mind mind env in
   Array.length (mib.mind_packets.(n).mind_consnames)
 
+let belongs_to_inductive (c : constructor) =
+  (* let env = Global.env () in *)
+  let glob_ref = Nametab.global c in
+  Globnames.isIndRef glob_ref
+
 module type Ord_ty_ctr_type = sig
   type t = ty_ctr 
   val compare : t -> t -> int
diff --git a/plugin/genericLib.mli b/plugin/genericLib.mli
index 8888f591e..0c31a4812 100644
--- a/plugin/genericLib.mli
+++ b/plugin/genericLib.mli
@@ -72,6 +72,7 @@ module type Ord_ctr_type = sig
 module Ord_ctr : Ord_ctr_type
 
 val num_of_ctrs : constructor -> int
+val belongs_to_inductive : constructor -> bool
 
 type ctr_rep = constructor * coq_type 
 val ctr_rep_to_string : ctr_rep -> string