From 99727f61d0a718e34d4282f9b9b45fce4336af84 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:15:18 +0000 Subject: [PATCH] is_top_down was not propageted correctly under a bottom-up conversion. --- .../components/content_pres/content2pres.ml | 41 +++++++++---------- 1 file changed, 20 insertions(+), 21 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 7d4839e03..ae7c8d46d 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -136,7 +136,7 @@ let rec justification term2pres p = Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)]) and proof2pres ?skip_initial_lambdas is_top_down term2pres p = - let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot = + let rec proof2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion = let indent = let is_decl e = (match e with @@ -152,18 +152,20 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = let body = let presconclude = conclude2pres - ?skip_initial_lambdas_internal: - (match skip_initial_lambdas_internal with - Some (`Later s) -> Some (`Now s) - | _ -> None) - is_top_down - p.Con.proof_name p.Con.proof_conclude indent omit_conclusion - omit_dot in + ?skip_initial_lambdas_internal: + (match skip_initial_lambdas_internal with + Some (`Later s) -> Some (`Now s) + | _ -> None) + is_top_down p.Con.proof_name p.Con.proof_conclude indent + omit_conclusion in_bu_conversion in let presacontext = acontext2pres - (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") - p.Con.proof_apply_context - presconclude indent + (if p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" then + is_top_down + else + false) + p.Con.proof_apply_context + presconclude indent (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") in context2pres @@ -172,6 +174,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> p.Con.proof_context) presacontext in +let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in match p.Con.proof_name with None -> body | Some name -> @@ -277,18 +280,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = [] -> in_bu_conversion | p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" in - let hd = - if indent then - B.indent (proof2pres is_top_down p in_bu_conversion) - else - proof2pres is_top_down p in_bu_conversion - in - B.V([Some "helm","xref",p.Con.proof_id], + let hd = proof2pres is_top_down p in_bu_conversion in + let hd = if indent then B.indent hd else hd in + B.V([Some "helm","xref",p.Con.proof_id], [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); continuation]) in aux ac - and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot = + and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion in_bu_conversion = let tconclude_body = match conclude.Con.conclude_conclusion with Some t (*when not omit_conclusion or @@ -342,14 +341,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.H([], [B.b_kw "done" ; B.Text([],".") ]) else B.b_hv [] - ((if not is_top_down || omit_dot then + ((if not is_top_down || in_bu_conversion then (make_concl "we proved" concl) :: if not is_top_down then let name = get_name ~default:"previous" name in [B.b_space; B.Text([],"(" ^ name ^ ")")] else [] else [B.b_kw "done"] - ) @ if not omit_dot then [B.Text([],".")] else []) + ) @ if not in_bu_conversion then [B.Text([],".")] else []) in B.V ([], prequel @ [conclude_body; ann_concl]) | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude -- 2.39.2