]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/acic2Procedural.ml
the level 1 reconstruction procedure is now in Procedural1
[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml
index 043bd6e3a6637cb0cb4915822c52013462467363..f749ce8d287eb3046f771b415c54ea42145bb6b5 100644 (file)
@@ -23,6 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
+module L    = Librarian
+
+module T  = ProceduralTypes
 module P1 = Procedural1
 module X  = ProceduralTeX
 
@@ -32,20 +35,13 @@ let tex_formatter = ref None
 
 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";
@@ -54,19 +50,12 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
 
 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)