Asking various models to generate `extract_record_computational_axioms` while implementing https://github.com/rocqetry/rocqet/pull/1

gpt5.ml

let extract_record_computational_axioms (ctx : LinkageCtx.t) : Libnames.qualid list =
  let rec collect (prefix : Libnames.qualid option) (linkage : Linkage.t)
      (acc : Libnames.qualid list) : Libnames.qualid list =
    let rec walk fields acc =
      match fields with
      | Bwd.Emp -> acc
      | Bwd.Snoc (rest, (field_name, elem)) ->
          let acc = walk rest acc in
          match elem with
          | LinkageElem.RecordComputationalAxiom { name; _ } ->
              let qualid = Naming.qualid_point prefix name in
              let qualid = Resolver.resolve_qualid ~context:ctx ~qualid in
              qualid :: acc
          | LinkageElem.FamilyDefinition { linkage = nested_linkage; _ } ->
              let new_prefix =
                match prefix with
                | None -> Libnames.qualid_of_ident field_name
                | Some p -> Naming.qualid_point (Some p) field_name
              in
              collect (Some new_prefix) nested_linkage acc
          | _ -> acc
    in
    walk linkage.fields acc
  in
  let linkage = Env.Context.family_linkage ctx in
  collect None linkage []

opus4-1.ml

let extract_record_computational_axioms (ctx : LinkageCtx.t) : Libnames.qualid list =
  let rec extract_from_linkage (linkage : Linkage.t) prefix_path =
    linkage.fields
    |> Bwd.to_list
    |> List.fold_left (fun acc (name, elem) ->
        let qualified_name = 
          match prefix_path with
          | [] -> Libnames.qualid_of_ident name
          | _ -> Naming.qualid_point (Some (Naming.list_to_path prefix_path)) name
        in
        match elem with
        | LinkageElem.RecordComputationalAxiom _ ->
            qualified_name :: acc
        | LinkageElem.FamilyDefinition { linkage = nested_linkage; _ } ->
            let nested_axioms = extract_from_linkage nested_linkage (prefix_path @ [name]) in
            nested_axioms @ acc
        | _ -> acc
      ) []
  in
  let rec extract_from_ctx = function
    | LinkageCtx.Toplevel linkage -> extract_from_linkage linkage []
    | LinkageCtx.Nested (parent_ctx, linkage) ->
        let parent_axioms = extract_from_ctx parent_ctx in
        let current_axioms = extract_from_linkage linkage [] in
        parent_axioms @ current_axioms
  in
  extract_from_ctx ctx

prompt.ml

(* We want to accumulate RecordComputationalAxiom in the current family *)
(* if we have Family we want to recursively check inside for RecordComputationalAxiom and append
   the appropriate path prefix *)
let extract_record_computational_axioms : LinkageCtx.t -> Libnames.qualid list =
  (* ... *)

sonnet3-5.ml

let rec extract_record_computational_axioms (ctx : LinkageCtx.t) : Libnames.qualid list =
  let rec extract_from_linkage (linkage : Linkage.t) (prefix : Libnames.qualid option) : Libnames.qualid list =
    let extract_from_field (field_name, elem) =
      match elem with
      | LinkageElem.RecordComputationalAxiom { name; _ } ->
          [Naming.qualid_point prefix name]
      | LinkageElem.FamilyDefinition { linkage = nested_linkage; _ } ->
          let nested_prefix = match prefix with
            | None -> Libnames.qualid_of_ident field_name
            | Some p -> Naming.qualid_point (Some p) field_name
          in
          extract_from_linkage nested_linkage (Some nested_prefix)
      | _ -> []
    in
    linkage.fields |> Bwd.to_list |> List.concat_map extract_from_field
  in
  match ctx with
  | LinkageCtx.Toplevel linkage -> extract_from_linkage linkage None
  | LinkageCtx.Nested (upper, linkage) ->
      let current = extract_from_linkage linkage None in
      let upper_axioms = extract_record_computational_axioms upper in
      current @ upper_axioms