-let proc_obj st = function
- | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
- let ast = proc_proof st v in
- let count = T.count_steps 0 ast in
- let text = Printf.sprintf "tactics: %u" count in
- T.Theorem (s, t, text) :: ast @ [T.Qed ""]
- | _ ->
- failwith "not a theorem"
+let def_flavours = [`Definition]
+
+let get_flavour ?flavour attrs =
+ let rec aux = function
+ | [] -> List.hd th_flavours
+ | `Flavour fl :: _ -> fl
+ | _ :: tl -> aux tl
+ in
+ match flavour with
+ | Some fl -> fl
+ | None -> aux attrs
+
+let proc_obj ?flavour ?(info="") st = function
+ | C.AConstant (_, _, s, Some v, t, [], attrs) ->
+ begin match get_flavour ?flavour attrs with
+ | flavour when List.mem flavour th_flavours ->
+ let ast = proc_proof st v in
+ let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
+ let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ 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) ->
+ [T.Inductive (types, lpsno, "")]
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"