-(* object costruction *******************************************************)
-
-let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
-
-let def_flavours = [`Definition; `Variant]
-
-let get_flavour st v attrs =
- let rec aux = function
- | [] ->
- if is_proof st 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 st.params with
- | Some fl -> fl
- | None -> aux attrs
-
-let proc_obj ?(info="") st = function
- | C.AConstant (_, _, s, Some v, t, [], attrs) ->
- begin match get_flavour st v 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"