(* proof construction *******************************************************)
-let anonymous_premise = C.Name "PREMISE"
+let anonymous_premise = C.Name "UNNAMED"
let mk_exp_args hd tl classes synth =
let meta id = C.AImplicit (id, None) in
let ity = H.acic_bc st.context ity in
let br1 = [T.Id ""] in
let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
- let text = "non linear rewrite" in
+ let text = "non-linear rewrite" in
st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
end
| _ -> assert false
| Some fl -> fl
| None -> aux attrs
-let proc_obj ?flavour st = function
+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 "tactics: %u\nnodes: %u" steps nodes 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, "")]
(* interface functions ******************************************************)
-let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
- ?flavour prefix anobj =
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
+ ?info ?depth ?flavour prefix anobj =
let st = {
sorts = ids_to_inner_sorts;
types = ids_to_inner_types;
} in
L.time_stamp "P : LEVEL 2 ";
HLog.debug "Procedural: level 2 transformation";
- let steps = proc_obj st ?flavour anobj in
+ let steps = proc_obj st ?flavour ?info anobj in
L.time_stamp "P : RENDERING";
HLog.debug "Procedural: grafite rendering";
let r = List.rev (T.render_steps [] steps) in