X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=63b4d4972281d0c5f5822cf4555ee54b86ff56ee;hb=HEAD;hp=f749ce8d287eb3046f771b415c54ea42145bb6b5;hpb=df3e9efe1690fb5d93061b657e6ddcc3c11745db;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index f749ce8d2..63b4d4972 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -23,22 +23,103 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module L    = Librarian
+module C  = Cic
+module L  = Librarian
+module G  = GrafiteAst
 
+module H  = ProceduralHelpers
 module T  = ProceduralTypes
 module P1 = Procedural1
+module P2 = Procedural2
 module X  = ProceduralTeX
 
 let tex_formatter = ref None
 
+(* object costruction *******************************************************)
+
+let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
+
+let def_flavours = [`Definition; `Variant]
+
+let get_flavour sorts params context v attrs =
+   let rec aux = function
+      | []               -> 
+         if H.is_acic_proof sorts context 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 params with
+      | 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 =
+	       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 ->
+            [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) ->
+      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"
+
 (* interface functions ******************************************************)
 
+let get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context =
+   let level_map x y = match x, y with
+      | None, G.IPLevel level -> Some level
+      | _                     -> x
+   in   
+   match List.fold_left level_map None params with
+      | None
+      | Some 2 ->   
+         P2.proc_proof 
+            (P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
+      | Some 1 ->
+         P1.proc_proof 
+            (P1.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
+      | Some n ->
+         failwith (
+	    "Procedural reconstruction level not supported: " ^ 
+	    string_of_int n
+	 )
+
 let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types 
-   ?info ?depth ?flavour prefix anobj = 
-   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 = P1.proc_obj st ?flavour ?info anobj in
+   ?info params anobj = 
+   let proc_proof = 
+      get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params []
+   in 
+   L.time_stamp "P : LEVEL 2  ";
+   HLog.debug "Procedural: level 2 transformation";
+   let steps = proc_obj ?info proc_proof ids_to_inner_sorts params [] anobj in
    let _ = match !tex_formatter with
       | None     -> ()
       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
@@ -48,14 +129,21 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
    let r = List.rev (T.render_steps [] steps) in
    L.time_stamp "P : DONE     "; r
 
-let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-   prefix context annterm = 
-   let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in
-   HLog.debug "Procedural: level 1 transformation";
-   let steps = P1.proc_proof st annterm in
+let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
+   context annterm = 
+   let proc_proof =
+      get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context
+   in
+   HLog.debug "Procedural: level 2 transformation";
+   let steps = proc_proof annterm in
    let _ = match !tex_formatter with
       | None     -> ()
       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
    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