Properly handle is_rec flag, fixing part of issue #117

Author: mattam82

src/equations.ml

@@ -406,25 +406,25 @@ let define_by_eqs opts eqs nt =
       | Struct -> StructuralOn i
       | Nested -> NestedOn (Some i)
     in
-    let rec_annot =
+    let is_rec, rec_annot =
       let default_recarg () =
 	let idx = List.length sign - 1 in
 	  (idx, None)
       in
       match rec_annot with
       | None ->
          (match is_rec with
-          | Some false -> Some (StructuralOn (default_recarg ()))
-          | _ -> None)
+          | Some false -> is_rec, Some (StructuralOn (default_recarg ()))
+          | _ -> is_rec, None)
       | Some (reck, None) ->
          (match is_recursive i [ieqs] with (* Recursive in its own body? *)
-          | Some _ -> Some (interp_reca reck (default_recarg ()))
-          | None -> if reck == Nested then Some (NestedOn None)
-                    else Some (StructuralOn (default_recarg ())))
+          | Some _ -> Some false, Some (interp_reca reck (default_recarg ()))
+          | None -> if reck == Nested then is_rec, Some (NestedOn None)
+                    else Some false, Some (StructuralOn (default_recarg ())))
       | Some (reck, Some lid) ->
          try
            let k, _, _ = lookup_rel_id (snd lid) sign in
-           Some (interp_reca reck (List.length sign - k, Some lid))
+           Some false, Some (interp_reca reck (List.length sign - k, Some lid))
          with Not_found ->
            user_err_loc (Some (fst lid), "struct_index",
                          Pp.(str"No argument named " ++ Id.print (snd lid) ++ str" found"))

test-suite/issues/issue117.v

@@ -0,0 +1,30 @@
+From Coq.Lists Require Import List.
+From Equations Require Import Equations.
+
+Inductive foo :=
+| Sum : list foo -> foo.
+
+Equations (struct t) do_foo1 (t: foo) : nat := {
+  do_foo1 (Sum u) :=
+        do_foo1_list2 u }
+
+  where (struct ts)
+    do_foo1_list (ts:list foo) : nat := {
+    do_foo1_list nil := 0;
+    do_foo1_list (cons t ts) := 0}
+
+  where (struct fs)
+    do_foo1_list2 (fs : list foo) : nat := {
+    do_foo1_list2 _ := 0}
+
+  where (struct t) do_foo2 (t : foo) : nat := {
+  do_foo2 _ := 0 }
+
+  where (struct ts)
+    do_foo2_list (ts:list foo) : nat := {
+    do_foo2_list nil := 0;
+    do_foo2_list (cons t ts) <= (do_foo2_list ts) => {
+      do_foo2_list (cons t _) _ := (do_foo1 t) + (do_foo2 t)}}.
+
+Next Obligation. destruct fs; reflexivity. Defined.
+Next Obligation. destruct t; reflexivity. Defined.