From 6baf07f7ebd9b40e642467f01a66920d9fb1448a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 24 Jul 2003 11:40:02 +0000 Subject: [PATCH] Improved management of conclusions, to avoid repetitions. Some problems of xrefs have been fixed. --- helm/ocaml/META.helm-cic_omdoc.src | 2 +- .../ocaml/cic_transformations/content2pres.ml | 138 ++++++++++++------ 2 files changed, 98 insertions(+), 42 deletions(-) diff --git a/helm/ocaml/META.helm-cic_omdoc.src b/helm/ocaml/META.helm-cic_omdoc.src index 313d19cd2..e05ddfcec 100644 --- a/helm/ocaml/META.helm-cic_omdoc.src +++ b/helm/ocaml/META.helm-cic_omdoc.src @@ -1,4 +1,4 @@ -requires="helm-cic_proof_checking" +requires="helm-cic_proof_checking helm-mathql_interpreter" version="0.0.1" archive(byte)="cic_omdoc.cma" archive(native)="cic_omdoc.cmxa" diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index da20856d2..cd7bac625 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -206,12 +206,14 @@ and proof2pres term2pres p = | `Hypothesis _ -> true | _ -> false) in ((List.filter is_decl p.Con.proof_context) != []) in + let omit_conclusion = (not indent) && (p.Con.proof_context != []) in let concl = (match p.Con.proof_conclude.Con.conclude_conclusion with None -> None | Some t -> Some (term2pres t)) in let body = - let presconclude = conclude2pres p.Con.proof_conclude indent in + let presconclude = + conclude2pres p.Con.proof_conclude indent omit_conclusion in let presacontext = acontext2pres p.Con.proof_apply_context presconclude indent in context2pres p.Con.proof_context presacontext in @@ -228,22 +230,39 @@ and proof2pres term2pres p = [(make_concl "proof of" ac); body]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left";Some "helm", "xref", p.Con.proof_id], + None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); P.Mtr ([],[P.Mtd ([], P.indented action)])]) +(* + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left";Some "helm", "xref", p.Con.proof_id], + [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); + P.Mtr ([],[P.Mtd ([], P.indented action)])]) *) and context2pres c continuation = (* we generate a subtable for each context element, for selection - purposes *) + purposes + The table generated by the head-element does not have an xref; + the whole context-proof is already selectable *) let module P = Mpresentation in - List.fold_right - (fun ce continuation -> - let xref = get_xref ce in + match c with + [] -> continuation + | hd::tl -> + let continuation' = + List.fold_right + (fun ce continuation -> + let xref = get_xref ce in + P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"; Some "helm", "xref", xref ], + [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]); + P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in + let hd_xref= get_xref hd in P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; Some "helm", "xref", xref ], - [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]); - P.Mtr([],[P.Mtd ([], continuation)])])) c continuation - + None,"columnalign","left"], + [P.Mtr([Some "helm", "xref", "ce_"^hd_xref], + [P.Mtd ([],ce2pres hd)]); + P.Mtr([],[P.Mtd ([], continuation')])]) + and ce2pres = let module P = Mpresentation in let module Con = Content in @@ -304,12 +323,29 @@ and proof2pres term2pres p = [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]); P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation - and conclude2pres conclude indent = + and conclude2pres conclude indent omit_conclusion = + let module Con = Content in let module P = Mpresentation in - if indent then - P.indented (conclude_aux conclude) + let tconclude_body = + match conclude.Con.conclude_conclusion with + Some t when not omit_conclusion -> + let concl = (term2pres t) in + if conclude.Con.conclude_method = "BU_Conversion" then + make_concl "that is equivalent to" concl + else + let conclude_body = conclude_aux conclude in + let ann_concl = make_concl "we conclude" concl in + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr ([],[P.Mtd ([],conclude_body)]); + P.Mtr ([],[P.Mtd ([],ann_concl)])]) + | _ -> conclude_aux conclude in + if indent then + P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id], + [tconclude_body])) else - conclude_aux conclude + P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) + and conclude_aux conclude = let module Con = Content in @@ -328,18 +364,12 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO SYNTH!!!") | Some c -> (term2pres c)) in P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]); P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]); P.Mtr([],[P.Mtd([],proof2pres subproof)])]) else if conclude.Con.conclude_method = "BU_Conversion" then - let conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in - make_concl - ~attrs:[Some "helm", "xref", conclude.Con.conclude_id] - "that is equivalent to" conclusion + assert false else if conclude.Con.conclude_method = "Exact" then let conclusion = (match conclude.Con.conclude_conclusion with @@ -349,9 +379,13 @@ and proof2pres term2pres p = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t | _ -> assert false) in - make_row ~attrs:[Some "helm", "xref", conclude.Con.conclude_id] + make_row [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion else if conclude.Con.conclude_method = "Intros+LetTac" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2pres p + | _ -> assert false) +(* OLD CODE let conclusion = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"NO Conclusion!!!") @@ -360,12 +394,12 @@ and proof2pres term2pres p = [Con.ArgProof p] -> P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; - Some "helm", "xref", conclude.Con.conclude_id], + None,"columnalign","left"], [P.Mtr([],[P.Mtd([],proof2pres p)]); P.Mtr([],[P.Mtd([], - (make_concl "we proved *" conclusion))])]); + (make_concl "we proved 1" conclusion))])]); | _ -> assert false) +*) else if (conclude.Con.conclude_method = "ByInduction") then byinduction conclude else if (conclude.Con.conclude_method = "Rewrite") then @@ -380,14 +414,23 @@ and proof2pres term2pres p = let term2 = (match List.nth conclude.Con.conclude_args 5 with Con.Term t -> term2pres t - | _ -> assert false) in + | _ -> assert false) in + P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ + P.Mtext([None,"mathcolor","Red"],"rewrite"); + P.Mspace([None,"width","0.1cm"]);term1; + P.Mspace([None,"width","0.1cm"]); + P.Mtext([None,"mathcolor","Red"],"with"); + P.Mspace([None,"width","0.1cm"]);term2]))]); + P.Mtr ([],[P.Mtd ([],P.indented justif)])]); +(* OLD CODE let conclusion = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"NO Conclusion!!!") | Some c -> term2pres c) in P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; - None,"columnalign","left"; - Some "helm", "xref", conclude.Con.conclude_id], + None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ P.Mtext([None,"mathcolor","Red"],"rewrite"); P.Mspace([None,"width","0.1cm"]);term1; @@ -395,10 +438,15 @@ and proof2pres term2pres p = P.Mtext([None,"mathcolor","Red"],"with"); P.Mspace([None,"width","0.1cm"]);term2]))]); P.Mtr ([],[P.Mtd ([],P.indented justif)]); - P.Mtr ([],[P.Mtd ([],make_concl "we proved" conclusion)])]) + P.Mtr ([],[P.Mtd ([],make_concl "we proved 2" conclusion)])]) *) else if conclude.Con.conclude_method = "Apply" then let pres_args = - make_args_for_apply term2pres conclude.Con.conclude_args in + make_args_for_apply term2pres conclude.Con.conclude_args in + P.Mrow([], + P.Mtext([None,"mathcolor","Red"],"by"):: + P.Mspace([None,"width","0.1cm"]):: + P.Mo([],"(")::pres_args@[P.Mo([],")")]) +(* OLD CODE let by = P.Mrow([], P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: @@ -407,15 +455,15 @@ and proof2pres term2pres p = None -> P.Mrow([],[P.Mtext([],"QUA");by]) | Some t -> let concl = (term2pres t) in - let ann_concl = make_concl "we proved" concl in + let ann_concl = make_concl "we proved 3" concl in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id], [P.Mtr ([],[P.Mtd ([],by)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) - else let body = + P.Mtr ([],[P.Mtd ([],ann_concl)])]) *) + else P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); P.Mtr ([], [P.Mtd ([], @@ -423,16 +471,17 @@ and proof2pres term2pres p = (P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - args2pres conclude.Con.conclude_args))))])]) in + args2pres conclude.Con.conclude_args))))])]) +(* OLD CODE match conclude.Con.conclude_conclusion with None -> body | Some t -> let concl = (term2pres t) in - let ann_concl = make_concl "we proved" concl in + let ann_concl = make_concl "we proved 4" concl in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],body)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) + P.Mtr ([],[P.Mtd ([],ann_concl)])]) *) and args2pres l = let module P = Mpresentation in @@ -489,14 +538,21 @@ and proof2pres term2pres p = (make_concl "we proceede by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in + P.Mtable + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + P.Mtr ([],[P.Mtd ([],induction_on)]):: + P.Mtr ([],[P.Mtd ([],to_prove)]):: + (make_cases args_for_cases)) +(* OLD CODE let we_proved = - (make_concl "we proved" proof_conclusion) in + (make_concl "we proved 5" proof_conclusion) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], P.Mtr ([],[P.Mtd ([],induction_on)]):: P.Mtr ([],[P.Mtd ([],to_prove)]):: (make_cases args_for_cases) @ - [P.Mtr ([],[P.Mtd ([],we_proved)])]) + [P.Mtr ([],[P.Mtd ([],we_proved)])]) *) and make_cases args_for_cases = let module P = Mpresentation in @@ -574,7 +630,7 @@ and proof2pres term2pres p = text::hyps) in (* let acontext = acontext2pres_old p.Con.proof_apply_context true in *) - let body = conclude2pres p.Con.proof_conclude true in + let body = conclude2pres p.Con.proof_conclude true false in let presacontext = P.Maction([None,"actiontype","toggle" ; None,"selection","1"], [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof")); -- 2.39.2