From c8767aa622ca1df27c537682e1d8694dc591d98a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 24 May 2007 15:52:48 +0000
Subject: [PATCH] added some flags to render subproofs (an hack)

---
 .../acic_procedural/acic2Procedural.ml        | 30 +++++++++++++++----
 .../acic_procedural/acic2Procedural.mli       |  3 +-
 2 files changed, 26 insertions(+), 7 deletions(-)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index d54130a0c..23b934d51 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -54,7 +54,9 @@ type status = {
    intros: string option list;
    clears: string list;
    clears_note: string;
-   case: int list
+   case: int list;
+   skip_thm_and_qed : bool;
+   skip_initial_lambdas : bool;
 }
 
 (* helpers ******************************************************************)
@@ -374,9 +376,14 @@ and proc_proof st t =
 	  (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) 
          | None          -> None, "\nNo types"
       in
-      let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
+      let context, clears = 
+        if st.skip_initial_lambdas then
+          st.context, []
+        else
+          Cn.get_clears st.context (H.cic t) xtypes 
+      in
       let note = Pp.ppcontext st.context ^ note in
-      {st with context = context; clears = clears; clears_note = note}
+      {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
       | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
@@ -422,13 +429,22 @@ let proc_obj st = function
       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
-      T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
+      let ast = 
+        if st.skip_initial_lambdas then 
+          match ast with
+            | T.Intros _::tl -> tl
+            | ast -> ast
+        else ast
+      in
+      if st.skip_thm_and_qed then ast
+      else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
 
 (* interface functions ******************************************************)
 
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = 
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+?(skip_thm_and_qed=false) ?(skip_initial_lambdas=false) prefix aobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -439,7 +455,9 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       intros      = [];
       clears      = [];
       clears_note = "";
-      case        = []
+      case        = [];
+      skip_thm_and_qed = skip_thm_and_qed;
+      skip_initial_lambdas = skip_initial_lambdas;
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in
diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli
index d1ff6a0c2..35092fb16 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.mli
+++ b/helm/software/components/acic_procedural/acic2Procedural.mli
@@ -26,7 +26,8 @@
 val acic2procedural:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
    ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> 
-   ?depth:int -> string -> Cic.annobj ->
+   ?depth:int -> ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool ->
+     string -> Cic.annobj ->
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list
-- 
2.39.2