From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:16:47 +0000 (+0000) Subject: 1. Code simplification X-Git-Tag: make_still_working~6220 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d214c33bbdc80874e65cbbadfd155019604856de;p=helm.git 1. Code simplification 2. Bug fixed: do not anticipate justification for rewritingLR or rewriting RL if justification is "exact" --- diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index ae7c8d46d..24c4faa34 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -121,18 +121,25 @@ let add_xref id = function | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) -let rec justification term2pres p = - if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or - ((p.Con.proof_context = []) & - (p.Con.proof_apply_context = []) & - (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then +let rec justification ~ignore_atoms term2pres p = + if p.Con.proof_conclude.Con.conclude_method = "Exact" && + ignore_atoms + then + [], None + else if + (p.Con.proof_conclude.Con.conclude_method = "Exact" && not ignore_atoms) || + (p.Con.proof_context = [] && + p.Con.proof_apply_context = [] && + p.Con.proof_conclude.Con.conclude_method = "Apply") + then let pres_args = - make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in - B.H([], - (B.b_kw "by")::B.b_space:: - B.Text([],"(")::pres_args@[B.Text([],")")]), None + make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args + in + [B.H([], + (B.b_kw "by")::B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")])], None else - B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"]), + [B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])], Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)]) and proof2pres ?skip_initial_lambdas is_top_down term2pres p = @@ -432,21 +439,37 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( || conclude.Con.conclude_method = "RewriteRL" then let justif1,justif2 = (match (List.nth conclude.Con.conclude_args 6) with - Con.ArgProof p -> justification term2pres p + Con.ArgProof p -> justification ~ignore_atoms:true term2pres p | _ -> assert false) in let justif = match justif2 with None -> justif1 - | Some j -> j + | Some j -> [j] + in + let index_term1, index_term2 = + if (conclude.Con.conclude_method = "RewriteLR" && is_top_down) + || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) + then 2,5 else 5,2 in let term1 = - (match List.nth conclude.Con.conclude_args 2 with + (match List.nth conclude.Con.conclude_args index_term1 with Con.Term (_,t) -> term2pres t | _ -> assert false) in let term2 = - (match List.nth conclude.Con.conclude_args 5 with + (match List.nth conclude.Con.conclude_args index_term2 with Con.Term (_,t) -> term2pres t | _ -> assert false) in + let justif = + match justif with + [] -> [] + | _ -> + justif @ + [B.V([], + [B.b_kw "we proved (" ; + term1 ; + B.b_kw "=" ; + term2; B.b_kw ") (equality)."])] + in (* B.V ([], B.H ([],[ @@ -457,17 +480,11 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.b_space; justif1]):: match justif2 with None -> [] | Some j -> [B.indent j]) *) - if (conclude.Con.conclude_method = "RewriteLR" && is_top_down) - || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then - B.V([], [justif ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"]) - else - B.V([], [justif ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"]) -(*CSC: bad idea - B.V([], [B.H([],[B.b_kw "obtain fooo " ; term2 ; B.b_kw "=" ; term1; B.b_kw "by" ; B.b_kw "proof" ; B.Text([],"."); justif1])]) *) + B.V([], justif @ [B.b_kw "by _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = - let j1,j2 = justification term2pres p in - [j1], match j2 with Some j -> [j] | None -> [] + let j1,j2 = justification ~ignore_atoms:false term2pres p in + j1, match j2 with Some j -> [j] | None -> [] in let rec aux args = match args with