Procedural: we added the support for rendering definitions and axioms

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index a6e0667b05de904d64209c177889ea06b3f37daa..298259cb56a7a9d45ce803c767534581a928f391 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -393,8 +393,9 @@ and proc_appl st what hd tl =
    mk_preamble st what script
 
 and proc_other st what =
+   let _, dtext = test_depth st in
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
-   let script = [T.Note text] in
+   let script = [T.Apply (what, dtext ^ text)] in 
    mk_preamble st what script
 
 and proc_proof st t = 
@@ -450,15 +451,22 @@ let is_theorem pars =
    List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
    List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
 
+let is_definition pars =
+   List.mem (`Flavour `Definition) pars
+
 let proc_obj st = function
-   | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
+   | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars    ->
       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
       if st.skip_thm_and_qed then ast
-      else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
-   | _                                                               ->
-      failwith "not a theorem"
+      else T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
+   | C.AConstant (_, _, s, Some v, t, [], pars) when is_definition pars ->
+      [T.Statement (`Definition, Some s, t, Some v, "")]
+   | C.AConstant (_, _, s, None, t, [], pars)                           ->
+      [T.Statement (`Axiom, Some s, t, None, "")]
+   | _                                                                  ->
+      failwith "not a theorem, definition, axiom"
 
 (* interface functions ******************************************************)