Merge PR coq#19107: Merging the code paths for fixpoint and cofixpoints

Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <[email protected]>
SkySkimmer · Jun 21, 2024 · 7ac876a · 7ac876a
2 parents daf6e20 + ef7d108
commit 7ac876a
Show file tree

Hide file tree

Showing 17 changed files with 194 additions and 229 deletions.
diff --git a/dev/ci/user-overlays/19107-herbelin-master+unify-fixpoint-cofixpoint-execution-paths.sh b/dev/ci/user-overlays/19107-herbelin-master+unify-fixpoint-cofixpoint-execution-paths.sh
@@ -0,0 +1,2 @@
+overlay coq_lsp https://github.com/herbelin/coq-lsp main+adapt-coq-pr19107-merge-fixpoint-cofixpoint 19107 herbelin-master+unify-fixpoint-cofixpoint-execution-paths
+overlay autosubst_ocaml https://github.com/herbelin/autosubst-ocaml master+adapt-coq-pr19107-merge-fixpoint-cofixpoint 19107 herbelin-master+unify-fixpoint-cofixpoint-execution-paths
diff --git a/interp/constrexpr.mli b/interp/constrexpr.mli
@@ -183,17 +183,17 @@ and branch_expr =
 
 and fix_expr =
   lident * relevance_info_expr
-  * recursion_order_expr option *
+  * fixpoint_order_expr option *
   local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
     lident * relevance_info_expr * local_binder_expr list * constr_expr * constr_expr
 
-and recursion_order_expr_r =
+and fixpoint_order_expr_r =
   | CStructRec of lident
   | CWfRec of lident * constr_expr
   | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
-and recursion_order_expr = recursion_order_expr_r CAst.t
+and fixpoint_order_expr = fixpoint_order_expr_r CAst.t
 
 (* Anonymous defs allowed ?? *)
 and local_binder_expr =

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
@@ -196,7 +196,7 @@ module Constr :
     val open_binders : local_binder_expr list Entry.t
     val one_open_binder : kinded_cases_pattern_expr Entry.t
     val one_closed_binder : kinded_cases_pattern_expr Entry.t
-    val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
+    val binders_fixannot : (local_binder_expr list * fixpoint_order_expr option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
     val arg : (constr_expr * explicitation CAst.t option) Entry.t

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
@@ -173,14 +173,12 @@ let () =
 
 let is_proof_termination_interactively_checked recsl =
   List.exists (function
-  | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } }
-      | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true
-  | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } }
-  | _, Vernacexpr.{ rec_order = None } -> false) recsl
+  | _, ( Some { CAst.v = (CMeasureRec _ | CWfRec _) }, _ ) -> true
+  | _, ( ( Some { CAst.v = CStructRec _ } | None), _) -> false) recsl
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacSynPure (VernacFixpoint(NoDischarge, List.map snd recsl))}))
+    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacSynPure (VernacFixpoint(NoDischarge, List.split (List.map snd recsl)))}))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
@@ -213,11 +211,11 @@ VERNAC COMMAND EXTEND Function STATE CUSTOM
     if is_interactive recsl then
       Vernactypes.vtopenproof (fun () ->
           CWarnings.with_warn warn
-            Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+            Gen_principle.do_generate_principle_interactive (List.split (List.map snd recsl)))
     else
       Vernactypes.vtdefault (fun () ->
           CWarnings.with_warn warn
-            Gen_principle.do_generate_principle (List.map snd recsl))
+            Gen_principle.do_generate_principle (List.split (List.map snd recsl)))
   }
 END
 

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
@@ -152,24 +152,14 @@ and rebuild_nal aux bk bl' nal typ =
 
 let rebuild_bl aux bl typ = rebuild_bl aux bl typ
 
-let recompute_binder_list fixpoint_exprl =
-  let fixl =
-    List.map
-      (fun fix ->
-        Vernacexpr.
-          { fix with
-            rec_order =
-              ComFixpoint.adjust_rec_order ~structonly:false fix.binders
-                fix.rec_order })
-      fixpoint_exprl
-  in
-  let (_, _, _, typel), _, ctx, _ =
-    ComFixpoint.interp_recursive ~check_recursivity:false ~cofix:false fixl
+let recompute_binder_list (rec_order, fixpoint_exprl) =
+  let _, _, ((_, _, _, typel), _, uctx, _) =
+    ComFixpoint.interp_recursive ~check_recursivity:false (false, CFixRecOrder rec_order) fixpoint_exprl
   in
   let constr_expr_typel =
     with_full_print
       (List.map (fun c ->
-           Constrextern.extern_constr (Global.env ()) (Evd.from_ctx ctx)
+           Constrextern.extern_constr (Global.env ()) (Evd.from_ctx uctx)
              (EConstr.of_constr c)))
       typel
   in
@@ -387,7 +377,7 @@ let generate_principle (evd : Evd.evar_map ref) pconstants on_error is_general
     end
   with e when CErrors.noncritical e -> on_error names e
 
-let register_struct is_rec fixpoint_exprl =
+let register_struct is_rec (rec_order, fixpoint_exprl) =
   let open EConstr in
   match fixpoint_exprl with
   | [{Vernacexpr.fname; univs; binders; rtype; body_def}] when not is_rec ->
@@ -416,7 +406,7 @@ let register_struct is_rec fixpoint_exprl =
     in
     (None, evd, List.rev rev_pconstants)
   | _ ->
-    let p = ComFixpoint.do_fixpoint ~poly:false fixpoint_exprl in
+    let p = ComFixpoint.do_mutually_recursive ~poly:false (CFixRecOrder rec_order, fixpoint_exprl) in
     assert (Option.is_empty p);
     let evd, rev_pconstants =
       List.fold_left
@@ -1748,20 +1738,18 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
     using_lemmas args ret_type body
 
 let do_generate_principle_aux pconstants on_error register_built
-    interactive_proof fixpoint_exprl : Declare.Proof.t option =
+    interactive_proof (rec_order, fixpoint_exprl as fix) : Declare.Proof.t option =
   List.iter
     (fun {Vernacexpr.notations} ->
       if not (List.is_empty notations) then
         CErrors.user_err (Pp.str "Function does not support notations for now"))
     fixpoint_exprl;
   let lemma, _is_struct =
-    match fixpoint_exprl with
-    | [ ( { Vernacexpr.rec_order =
-              Some {CAst.v = Constrexpr.CWfRec (wf_x, wf_rel)} } as
-        fixpoint_expr ) ] ->
+    match rec_order with
+    | [ Some { CAst.v = Constrexpr.CWfRec (wf_x, wf_rel) } ] ->
       let ( {Vernacexpr.fname; univs = _; binders; rtype; body_def} as
           fixpoint_expr ) =
-        match recompute_binder_list [fixpoint_expr] with
+        match recompute_binder_list fix with
         | [e] -> e
         | _ -> assert false
       in
@@ -1785,12 +1773,10 @@ let do_generate_principle_aux pconstants on_error register_built
             wf_x.CAst.v using_lemmas binders rtype body pre_hook
         , false )
       else (None, false)
-    | [ ( { Vernacexpr.rec_order =
-              Some {CAst.v = Constrexpr.CMeasureRec (wf_x, wf_mes, wf_rel_opt)}
-          } as fixpoint_expr ) ] ->
+    | [ Some { CAst.v = Constrexpr.CMeasureRec (wf_x, wf_mes, wf_rel_opt) } ] ->
       let ( {Vernacexpr.fname; univs = _; binders; rtype; body_def} as
           fixpoint_expr ) =
-        match recompute_binder_list [fixpoint_expr] with
+        match recompute_binder_list fix with
         | [e] -> e
         | _ -> assert false
       in
@@ -1818,24 +1804,22 @@ let do_generate_principle_aux pconstants on_error register_built
     | _ ->
       List.iter
         (function
-          | {Vernacexpr.rec_order} -> (
-            match rec_order with
-            | Some {CAst.v = Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _} ->
+            | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
               CErrors.user_err
                 (Pp.str
                    "Cannot use mutual definition with well-founded recursion \
                     or measure")
-            | _ -> () ))
-        fixpoint_exprl;
-      let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
+            | _ -> () )
+        rec_order;
+      let fixpoint_exprl = recompute_binder_list fix in
       let fix_names =
         List.map (function {Vernacexpr.fname} -> fname.CAst.v) fixpoint_exprl
       in
       (* ok all the expressions are structural *)
       let recdefs, _rec_impls = build_newrecursive fixpoint_exprl in
       let is_rec = List.exists (is_rec fix_names) recdefs in
       let lemma, evd, pconstants =
-        if register_built then register_struct is_rec fixpoint_exprl
+        if register_built then register_struct is_rec (rec_order, fixpoint_exprl)
         else (None, Evd.from_env (Global.env ()), pconstants)
       in
       let evd = ref evd in
@@ -2103,9 +2087,9 @@ let make_graph (f_ref : GlobRef.t) =
                      nal_tas)
               in
               let b' = add_args id.CAst.v new_args b in
+              Some (CAst.make (CStructRec (CAst.make rec_id))),
               { Vernacexpr.fname = id
               ; univs = None
-              ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id)))
               ; binders = nal_tas @ bl
               ; rtype = t
               ; body_def = Some b'
@@ -2115,15 +2099,15 @@ let make_graph (f_ref : GlobRef.t) =
         l
       | _ ->
         let fname = CAst.make (Label.to_id (Constant.label c)) in
-        [ { Vernacexpr.fname
+        [ None, { Vernacexpr.fname
           ; univs = None
-          ; rec_order = None
           ; binders = nal_tas
           ; rtype = t
           ; body_def = Some b
           ; notations = [] } ]
     in
     let mp = Constant.modpath c in
+    let expr_list = List.split expr_list in
     let pstate =
       do_generate_principle_aux [(c, UVars.Instance.empty)] error_error false
         false expr_list
@@ -2133,7 +2117,7 @@ let make_graph (f_ref : GlobRef.t) =
     List.iter
       (fun {Vernacexpr.fname = {CAst.v = id}} ->
         add_Function false (Constant.make2 mp (Label.of_id id)))
-      expr_list
+      (snd expr_list)
 
 (* *************** statically typed entrypoints ************************* *)
 

diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
@@ -12,9 +12,9 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle_interactive :
-  Vernacexpr.fixpoint_expr list -> Declare.Proof.t
+  Vernacexpr.fixpoints_expr -> Declare.Proof.t
 
-val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
+val do_generate_principle : Vernacexpr.fixpoints_expr -> unit
 val make_graph : Names.GlobRef.t -> unit
 
 (* Can be thrown by build_{,case}_scheme *)

diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
@@ -36,7 +36,7 @@ val pr_sort_expr : sort_expr -> Pp.t
 val pr_guard_annot
   :  (constr_expr -> Pp.t)
   -> local_binder_expr list
-  -> recursion_order_expr option
+  -> fixpoint_order_expr option
   -> Pp.t
 
 val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		overlay coq_lsp https://github.com/herbelin/coq-lsp main+adapt-coq-pr19107-merge-fixpoint-cofixpoint 19107 herbelin-master+unify-fixpoint-cofixpoint-execution-paths
		overlay autosubst_ocaml https://github.com/herbelin/autosubst-ocaml master+adapt-coq-pr19107-merge-fixpoint-cofixpoint 19107 herbelin-master+unify-fixpoint-cofixpoint-execution-paths