| 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 = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
- "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ 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 ->
| C.AConstant (_, _, s, None, t, [], attrs) ->
[T.Statement (`Axiom, Some s, t, None, "")]
| C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
- [T.Inductive (types, lpsno, "")]
+ 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"
in
HLog.debug "Procedural: grafite rendering";
List.rev (T.render_steps [] steps)
+
+let rec is_debug n = function
+ | [] -> false
+ | G.IPDebug debug :: _ -> n <= debug
+ | _ :: tl -> is_debug n tl