From c8767aa622ca1df27c537682e1d8694dc591d98a Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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