* http://cs.unibo.it/helm/.
*)
+module L = Librarian
+
+module T = ProceduralTypes
module P1 = Procedural1
module X = ProceduralTeX
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;
- max_depth = depth;
- depth = 0;
- context = [];
- case = []
- } in
+ let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in
L.time_stamp "P : LEVEL 1 ";
HLog.debug "Procedural: level 1 transformation";
- let steps = proc_obj st ?flavour ?info anobj in
+ let steps = P1.proc_obj st ?flavour ?info anobj in
let _ = match !tex_formatter with
| None -> ()
- | Some frm -> X.tex_of_steps frm st.sorts steps
+ | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
in
L.time_stamp "P : RENDERING";
HLog.debug "Procedural: grafite rendering";
let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
prefix context annterm =
- let st = {
- sorts = ids_to_inner_sorts;
- types = ids_to_inner_types;
- max_depth = depth;
- depth = 0;
- context = context;
- case = []
- } in
+ let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in
HLog.debug "Procedural: level 1 transformation";
- let steps = proc_proof st annterm in
+ let steps = P1.proc_proof st annterm in
let _ = match !tex_formatter with
| None -> ()
- | Some frm -> X.tex_of_steps frm st.sorts steps
+ | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
in
HLog.debug "Procedural: grafite rendering";
List.rev (T.render_steps [] steps)