[Subsumed] Towards a single code path for the "using" clause + small improvement of "using Type" for co/fixpoints

dev/ci/user-overlays/18742-herbelin-master+one-copy-of-using-clause.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr18742-using-moved-from-cinfo-to-info 18742 master+one-copy-of-using-clause

test-suite/success/definition_using.v

@@ -80,3 +80,43 @@ End B.
 Check c8 : forall a, c1 a = true -> bogus.
 Check c9 : forall a, c1 a = true -> bogus.
 Check c10: bogus -> bogus.
+
+Module TypeBehavior.
+
+Section S.
+Variables a : nat.
+#[using="Type", warning="-non-recursive"]
+Program Fixpoint b1 (n:nat) : nat := (fun _ => 0) a.
+Program Fixpoint b2 (n:nat) : (fun X _ => X) nat a := 0.
+Program Fixpoint b3 (n:nat) : (fun X _ => X) nat a := (fun _ => 0) a.
+Program Definition c1 : nat := (fun _ => 0) a.
+Program Definition c2 : (fun X _ => X) nat a := 0.
+Program Definition c3 : (fun X _ => X) nat a := (fun _ => 0) a.
+Fixpoint d1 (n:nat) : nat := (fun _ => 0) a.
+Fixpoint d2 (n:nat) : (fun X _ => X) nat a := 0.
+Fixpoint d3 (n:nat) : (fun X _ => X) nat a := (fun _ => 0) a.
+Definition e1 : nat := (fun _ => 0) a.
+Definition e2 : (fun X _ => X) nat a := 0.
+Definition e3 : (fun X _ => X) nat a := (fun _ => 0) a.
+End S.
+(* Not clear what is most expected below... *)
+
+(* Dependency in a with Program Fixpoint: the body is not reduced. *)
+Check b1 0 0 : nat.
+(* No dependency in a with Program Fixpoint, because both body and type are beta-reduced *)
+(* Why there is a difference with b1 is not clear *)
+Check b2 0 : nat.
+Check b3 0 : nat.
+(* With Program Definition, type is beta-reduced but not the body *)
+Check c1 0 : nat.
+Check c2 : nat.
+Check c3 0 : nat.
+(* With Definition/Fixpoint, neither body nor type are beta-reduced *)
+Check d1 0 0 : nat.
+Check d2 0 0 : nat.
+Check d3 0 0 : nat.
+Check e1 0 : nat.
+Check e2 0 : nat.
+Check e3 0 : nat.
+
+End TypeBehavior.

test-suite/success/proof_using.v

@@ -195,4 +195,61 @@ Qed.
 End Clear.
 *)
 
+Module InteractiveUsing.
 
+Section S.
+
+Variable m : nat.
+Variable e : m = m.
+
+#[using="e"]
+Definition a := 0.
+
+#[using="e"]
+Definition a' : nat.
+exact 0.
+Defined.
+
+#[using="e"]
+Fixpoint f (n:nat) : nat :=
+ match n with 0 => 0 | S n => f n end.
+
+#[using="e"]
+Fixpoint f' (n:nat) : nat.
+exact (match n with 0 => 0 | S n => f n end).
+Defined.
+
+#[using="Type"]
+Fixpoint f1 (n:nat) : nat :=
+  match n with 0 => 0 | S n => match f2 n with eq_refl => n end end
+with f2 (n:nat) : m = m :=
+  match n with 0 => eq_refl | S n => match f1 n with 0 => eq_refl | S _ => eq_refl end end.
+
+#[using="Type"]
+Fixpoint f1' (n:nat) : nat with f2' (n:nat) : m = m.
+exact (match n with 0 => 0 | S n => match f2' n with eq_refl => n end end).
+exact (match n with 0 => eq_refl | S n => match f1' n with 0 => eq_refl | S _ => eq_refl end end).
+Defined.
+
+CoInductive Stream : Set := Cons : Stream -> Stream.
+
+#[using="e"]
+CoFixpoint g : Stream := Cons g.
+
+#[using="e"]
+CoFixpoint g' : Stream.
+exact (Cons g).
+Defined.
+
+End S.
+
+Check eq_refl : a 0 (eq_refl 0) = 0.
+Check eq_refl : a' 0 (eq_refl 0) = 0.
+Check eq_refl : f 10 (eq_refl 10) 2 = 0.
+Check eq_refl : f' 10 (eq_refl 10) 2 = 0.
+Check eq_refl : f1 10 2 = 1.
+Check eq_refl : f1' 10 2 = 1.
+Check g 0 eq_refl : Stream.
+Check g' 0 eq_refl : Stream.
+
+End InteractiveUsing.

vernac/comDefinition.ml

@@ -126,8 +126,8 @@ let do_definition ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using
   in
   let using = definition_using env evd ~body ~types ~using in
   let kind = Decls.IsDefinition kind in
-  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
-  let info = Declare.Info.make ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns () in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let info = Declare.Info.make ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns ?using () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
@@ -151,7 +151,7 @@ let do_definition_program ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags
   let using = definition_using env evd ~body ~types ~using in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
-    let info = Declare.Info.make ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let info = Declare.Info.make ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns ?using () in
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
   in pm

vernac/comFixpoint.ml

@@ -259,39 +259,40 @@ let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let build_recthms ~indexes ?using fixnames fixtypes fiximps =
+let build_recthms ~indexes ?using fixnames fixdefs fixtypes fiximps =
   let fix_kind, cofix = match indexes with
     | Some indexes -> Decls.Fixpoint, false
     | None -> Decls.CoFixpoint, true
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        let env = Global.env() in
-        let evd = Evd.from_env env in
-        let terms = [EConstr.of_constr typ] in
-        let using = Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
         let args = List.map Context.Rel.Declaration.get_name ctx in
-        Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
+        Declare.CInfo.make ~name ~typ ~args ~impargs ()
       ) fixnames fixtypes fiximps
   in
-  fix_kind, cofix, thms
-
-let declare_fixpoint_interactive_generic ?indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
-  let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
+  let using =
+    let env = Global.env() in
+    let evd = Evd.from_env env in
+    let terms = List.map EConstr.of_constr (fixtypes @ List.map_filter (fun x -> x) fixdefs) in
+    Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
+  fix_kind, cofix, thms, using
+
+let declare_fixpoint_interactive_generic ?indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+  let fix_kind, cofix, thms, using = build_recthms ~indexes ?using fixnames fixdefs fixtypes fiximps in
   let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
-  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags ?user_warns ~ntns ?using () in
   Declare.Proof.start_mutual_with_initialization ~info
     evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None
 
 let declare_fixpoint_generic ?indexes ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
-  let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
+  let fix_kind, cofix, fixitems, using = build_recthms ~indexes ?using fixnames fixdefs fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
-  let info = Declare.Info.make ?scope ?clearbody ~kind:fix_kind ~poly ~udecl ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ?scope ?clearbody ~kind:fix_kind ~poly ~udecl ?typing_flags ?user_warns ~ntns ?using () in
   let cinfo = fixitems in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
@@ -331,9 +332,9 @@ let do_fixpoint_common ?typing_flags (fixl : Vernacexpr.fixpoint_expr list) =
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false ?typing_flags fixl in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
-let do_fixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns l : Declare.Proof.t =
+let do_fixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l : Declare.Proof.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
-  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns fix ntns in
+  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix ntns in
   lemma
 
 let do_fixpoint ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
@@ -345,9 +346,9 @@ let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
   interp_fixpoint ~cofix:true fixl, ntns
 
-let do_cofixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns l =
+let do_cofixpoint_interactive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
   let cofix, ntns = do_cofixpoint_common l in
-  let lemma = declare_fixpoint_interactive_generic ~scope ?clearbody ~poly ?typing_flags ?user_warns cofix ntns in
+  let lemma = declare_fixpoint_interactive_generic ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using cofix ntns in
   lemma
 
 let do_cofixpoint ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =

vernac/comFixpoint.mli

@@ -21,6 +21,7 @@ val do_fixpoint_interactive
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
+  -> ?using:Vernacexpr.section_subset_expr
   -> fixpoint_expr list
   -> Declare.Proof.t
 
@@ -40,6 +41,7 @@ val do_cofixpoint_interactive
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
+  -> ?using:Vernacexpr.section_subset_expr
   -> cofixpoint_expr list
   -> Declare.Proof.t
 

vernac/comProgramFixpoint.ml

@@ -208,9 +208,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) ?scope ?clearbody poly ?typ
     Option.map (fun using -> Proof_using.definition_using env sigma ~fixnames:[] ~using ~terms) using
   in
   let uctx = Evd.evar_universe_context sigma in
-  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
+  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
   let kind = Decls.(IsDefinition Fixpoint) in
-  let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ~hook ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ~hook ?typing_flags ?user_warns ?using ~ntns () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
   pm
@@ -237,20 +237,21 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
-    let terms = [def; typ] in
-    let using = Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
     let def = nf_evar evd (EConstr.it_mkNamedLambda_or_LetIn evd def rec_sign) in
     let typ = nf_evar evd (EConstr.it_mkNamedProd_or_LetIn evd typ rec_sign) in
     let deps = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evd
         (List.length rec_sign) ~deps def typ in
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
     (cinfo, def, evars)
   in
   let fiximps = List.map pi2 info in
   let fixdefs = List.map out_def fixdefs in
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
+  let using =
+    let terms = fixdefs @ fixtypes in
+    Option.map (fun using -> Proof_using.definition_using env evd ~fixnames ~using ~terms) using in
   let () = if not cofix then begin
       let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in
       (* XXX: are we allowed to have evars here? *)
@@ -278,7 +279,7 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
   | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
-  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns () in
+  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns ?using () in
   Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx fixkind
 
 let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =