+(* object costruction *******************************************************)
+
+let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
+
+let def_flavours = [`Definition; `Variant]
+
+let get_flavour sorts params context v attrs =
+ let rec aux = function
+ | [] ->
+ if H.is_acic_proof sorts context v then List.hd th_flavours
+ else List.hd def_flavours
+ | `Flavour fl :: _ -> fl
+ | _ :: tl -> aux tl
+ in
+ let flavour_map x y = match x, y with
+ | None, G.IPAs flavour -> Some flavour
+ | _ -> x
+ in
+ match List.fold_left flavour_map None params with
+ | Some fl -> fl
+ | None -> aux attrs
+
+let rec is_record = function
+ | [] -> None
+ | `Class (`Record fields) :: _ -> Some fields
+ | _ :: tl -> is_record tl
+
+let proc_obj ?(info="") proc_proof sorts params context = function
+ | C.AConstant (_, _, s, Some v, t, [], attrs) ->
+ begin match get_flavour sorts params context v attrs with
+ | flavour when List.mem flavour th_flavours ->
+ let ast = proc_proof v in
+ let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
+ let text =
+ if List.mem G.IPComments params then
+ Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ else
+ ""
+ in
+ T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
+ | flavour when List.mem flavour def_flavours ->
+ [T.Statement (flavour, Some s, t, Some v, "")]
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"
+ end
+ | C.AConstant (_, _, s, None, t, [], attrs) ->
+ [T.Statement (`Axiom, Some s, t, None, "")]
+ | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
+ begin match is_record attrs with
+ | None -> [T.Inductive (types, lpsno, "")]
+ | Some fs -> [T.Record (types, lpsno, fs, "")]
+ end
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"
+