X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=45e88ab0a26a9fc5626fc1a86bf6565d2477a9df;hb=1ca5e357b247833e561be0f0760d18d705d4f1d6;hp=a41ccc99158a73562218887d2d786e57d903121e;hpb=66929b8edb58d468a134b648466f3e9c45ba5c0e;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index a41ccc991..45e88ab0a 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -113,9 +113,9 @@ let make_args_for_apply term2pres args = (List.fold_right (make_arg_for_apply false) tl []) | _ -> assert false -let get_name = function +let get_name ?(default="_") = function | Some s -> s - | None -> "_" + | None -> default let add_xref id = function | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) @@ -131,8 +131,10 @@ let rec justification term2pres p = B.H([], (B.b_kw "by")::B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")]), None - else (B.b_kw "by"), - Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p]) + else + (*(B.b_kw "by"), + Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])*) + proof2pres true term2pres p, None and proof2pres ?skip_initial_lambdas is_top_down term2pres p = let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot = @@ -257,17 +259,35 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = term]) and acontext2pres is_top_down ac continuation indent in_bu_conversion = - List.fold_right - (fun p continuation -> + let rec aux = + function + [] -> continuation + | p::tl -> + let continuation = aux tl in + (* Applicative context get flattened and the "body" of a BU_Conversion + is put in the applicative context. Thus two different situations + are possible: + {method = "BU_Conversion"; applicative_context=[p1; ...; pn]} + {method = xxx; applicative_context = + [ p1; ...; pn; {method="BU_Conversion"} ; p_{n+1}; ... ; pm ]} + In both situations only pn must be processed in in_bu_conversion + mode + *) + let in_bu_conversion = + match tl with + [] -> 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], - [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); - continuation])) ac continuation + 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 = let tconclude_body = @@ -283,18 +303,15 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.b_hv [] (make_concl "that is equivalent to" concl :: if is_top_down then [B.b_space ; B.b_kw "done"; - B.Text([],".")] else []) + B.Text([],".")] else [B.Text([],".")]) else if conclude.Con.conclude_method = "FalseInd" then (* false ind is in charge to add the conclusion *) falseind conclude else let prequel = if - (match skip_initial_lambdas_internal with - None - | Some (`Later _) -> true - | Some (`Now _) -> false) - && conclude.Con.conclude_method = "Intros+LetTac" + (not is_top_down) && + conclude.Con.conclude_method = "Intros+LetTac" then let name = get_name name in [B.V ([], @@ -314,7 +331,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = else [] in let conclude_body = - conclude_aux ?skip_initial_lambdas_internal conclude in + conclude_aux ?skip_initial_lambdas_internal is_top_down conclude in let ann_concl = if conclude.Con.conclude_method = "Intros+LetTac" || conclude.Con.conclude_method = "ByInduction" @@ -323,13 +340,19 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.Text([],"") else if omit_conclusion then B.H([], [B.b_kw "done" ; B.Text([],".") ]) - else B.b_hv [] - ((if not is_top_down || omit_dot then [make_concl "we proved" - concl; B.Text([],if not is_top_down then "(previous)" else "")] - else [B.b_kw "done"]) @ if not omit_dot then [B.Text([],".")] else []) + else + B.b_hv [] + ((if not is_top_down || omit_dot 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 []) in - B.V ([], prequel @ [conclude_body; ann_concl]) - | _ -> conclude_aux ?skip_initial_lambdas_internal conclude + B.V ([], prequel @ [conclude_body; ann_concl]) + | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude in if indent then B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], @@ -337,7 +360,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = else B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - and conclude_aux ?skip_initial_lambdas_internal conclude = + and conclude_aux ?skip_initial_lambdas_internal is_top_down conclude = if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with @@ -354,8 +377,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.V ([], [make_concl "we need to prove" expected; - make_concl "or equivalently" synth; - B.Text([],"."); + B.H ([],[make_concl "or equivalently" synth; B.Text([],".")]); proof2pres true subproof false]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false @@ -407,7 +429,8 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = andind conclude else if (conclude.Con.conclude_method = "FalseInd") then falseind conclude - else if (conclude.Con.conclude_method = "Rewrite") then + else if conclude.Con.conclude_method = "RewriteLR" + || conclude.Con.conclude_method = "RewriteRL" then let justif1,justif2 = (match (List.nth conclude.Con.conclude_args 6) with Con.ArgProof p -> justification term2pres p @@ -429,7 +452,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.b_space; term2; B.b_space; justif1]):: match justif2 with None -> [] | Some j -> [B.indent j]) -*) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"]) +*) + if (conclude.Con.conclude_method = "RewriteLR" && is_top_down) + || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then + B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"]) + else + B.V([], [justif1 ; 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])]) *) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = (* @@ -495,7 +525,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.b_kw "the previous result" + None -> B.b_kw "previous" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term (_,t) -> @@ -526,7 +556,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.b_kw "the previous result" + None -> B.b_kw "previous" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term (_,t) -> @@ -535,8 +565,8 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | Con.ArgMethod s -> B.b_kw "a method???") in (make_concl "we proceed by induction on" arg) in let to_prove = - (make_concl "to prove" proof_conclusion) in - B.V ([], induction_on::to_prove:: B.Text([],".")::(make_cases args_for_cases)) + B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in + B.V ([], induction_on::to_prove::(make_cases args_for_cases)) and make_cases l = List.map make_case l @@ -600,8 +630,6 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> assert false in let hyps = List.map make_hyp indhyps in text::hyps) in - (* let acontext = - acontext2pres_old p.Con.proof_apply_context true in *) let body = conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in let presacontext = @@ -617,7 +645,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = p.Con.proof_apply_context body true (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") ]) in - B.V ([], pattern::induction_hypothesis@[asubconcl;B.Text([],".");presacontext]) + B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext]) | _ -> assert false and falseind conclude = @@ -645,7 +673,6 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.b_kw "is contradictory, hence" ] | _ -> assert false) in - (* let body = proof2pres {proof with Con.proof_context = tl} false in *) make_row arg proof_conclusion and andind conclude = @@ -683,8 +710,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.Text([],")"); B.skip; term2pres hyp2.Con.dec_type]) in - (* let body = proof2pres {proof with Con.proof_context = tl} false in *) - let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in + let body = + conclude2pres false proof.Con.proof_name proof.Con.proof_conclude + false true false in let presacontext = acontext2pres false proof.Con.proof_apply_context body false false in @@ -723,8 +751,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.Text([],")"); B.skip; term2pres hyp.Con.dec_type]) in - (* let body = proof2pres {proof with Con.proof_context = tl} false in *) - let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in + let body = + conclude2pres false proof.Con.proof_name proof.Con.proof_conclude + false true false in let presacontext = acontext2pres false proof.Con.proof_apply_context body false false in @@ -872,7 +901,7 @@ let content2pres [Some "helm","xref","id"] ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: params2pres params @ [B.b_kw ":"]); - B.indent (term2pres thesis) ; B.b_kw "." ] @ + B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @ metasenv2pres term2pres metasenv @ [proof ; B.b_kw "qed."]) | `Def (_, ty, `Definition body) ->