X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=575bb687af1eea1966a5aa59138b26afacc06e45;hb=60f8a4de1287ea04ee5722460bdc6ff16a3eb4be;hp=cd7bac62544b101ad2be9b0d61e30d21e559713b;hpb=6baf07f7ebd9b40e642467f01a66920d9fb1448a;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index cd7bac625..575bb687a 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -192,7 +192,7 @@ let rec justification term2pres p = make_args_for_apply term2pres p.Con.proof_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([],")")]) + P.Mtext([],"(")::pres_args@[P.Mtext([],")")]) else proof2pres term2pres p and proof2pres term2pres p = @@ -220,15 +220,19 @@ and proof2pres term2pres p = match p.Con.proof_name with None -> body | Some name -> - let ac = - (match concl with - None -> P.Mtext([],"NO PROOF!!!") - | Some c -> c) in let action = - P.Maction([None,"actiontype","toggle" ; - None,"selection","1"], - [(make_concl "proof of" ac); - body]) in + match concl with + None -> body +(* + P.Maction + ([None,"actiontype","toggle" ; None,"selection","1"], + [P.Mtext [] "proof" ; body]) +*) + | Some ac -> + P.Maction + ([None,"actiontype","toggle" ; None,"selection","1"], + [(make_concl "proof of" ac); body]) + in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); @@ -293,7 +297,11 @@ and proof2pres term2pres p = ty]) | None -> prerr_endline "NO NAME!!"; assert false) - | `Proof p -> proof2pres p + | `Proof p -> + (match p.Con.proof_name with + Some "w" -> prerr_endline ("processing w"); + | _ -> ()); + proof2pres p | `Definition d -> (match d.Con.def_name with Some s -> @@ -334,7 +342,10 @@ and proof2pres term2pres p = make_concl "that is equivalent to" concl else let conclude_body = conclude_aux conclude in - let ann_concl = make_concl "we conclude" concl in + let ann_concl = + if conclude.Con.conclude_method = "TD_Conversion" then + make_concl "that is equivalent to" concl + else make_concl "we conclude" concl in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],conclude_body)]); @@ -371,16 +382,19 @@ and proof2pres term2pres p = else if conclude.Con.conclude_method = "BU_Conversion" then assert false else if conclude.Con.conclude_method = "Exact" then - let conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in let arg = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t | _ -> assert false) in - make_row - [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion + (match conclude.Con.conclude_conclusion with + None -> + P.Mrow [] + [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] + | Some c -> let conclusion = term2pres c in + 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 @@ -402,6 +416,10 @@ and proof2pres term2pres p = *) else if (conclude.Con.conclude_method = "ByInduction") then byinduction conclude + else if (conclude.Con.conclude_method = "Exists") then + exists conclude + else if (conclude.Con.conclude_method = "AndInd") then + andind conclude else if (conclude.Con.conclude_method = "Rewrite") then let justif = (match (List.nth conclude.Con.conclude_args 6) with @@ -544,16 +562,7 @@ and proof2pres term2pres p = 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 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)])]) *) - + and make_cases args_for_cases = let module P = Mpresentation in List.map @@ -639,7 +648,114 @@ and proof2pres term2pres p = None,"columnalign","left"], pattern::asubconcl::induction_hypothesis@ [P.Mtr([],[P.Mtd([],presacontext)])]) - | _ -> assert false in + | _ -> assert false + + and andind conclude = + let module P = Mpresentation in + let module Con = Content in + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"No conclusion???") + | Some t -> term2pres t) in + let proof,case_arg = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + let arg = + (match case_arg with + Con.Aux n -> assert false + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> [] + | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)]) + | Con.Lemma lemma -> + [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)] + | _ -> assert false) in + match proof.Con.proof_context with + `Hypothesis hyp1::`Hypothesis hyp2::tl -> + let get_name hyp = + (match hyp.Con.dec_name with + None -> "_" + | Some s -> s) in + let preshyp1 = + P.Mrow ([], + [P.Mtext([],"("); + P.Mi([],get_name hyp1); + P.Mtext([],")"); + P.smallskip; + term2pres hyp1.Con.dec_type]) in + let preshyp2 = + P.Mrow ([], + [P.Mtext([],"("); + P.Mi([],get_name hyp2); + P.Mtext([],")"); + P.smallskip; + term2pres hyp2.Con.dec_type]) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + let body = conclude2pres proof.Con.proof_conclude false true in + let presacontext = + acontext2pres proof.Con.proof_apply_context body false in + P.Mtable + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr ([],[P.Mtd ([], + P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]); + P.Mtr ([],[P.Mtd ([],preshyp1)]); + P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]); + P.Mtr ([],[P.Mtd ([],preshyp2)]); + P.Mtr ([],[P.Mtd ([],presacontext)])]); + | _ -> assert false + + and exists conclude = + let module P = Mpresentation in + let module Con = Content in + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"No conclusion???") + | Some t -> term2pres t) in + let proof = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;Con.ArgProof proof;_] -> proof + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + match proof.Con.proof_context with + `Declaration decl::`Hypothesis hyp::tl + | `Hypothesis decl::`Hypothesis hyp::tl -> + let get_name decl = + (match decl.Con.dec_name with + None -> "_" + | Some s -> s) in + let presdecl = + P.Mrow ([], + [P.Mtext([None,"mathcolor","Red"],"let"); + P.smallskip; + P.Mi([],get_name decl); + P.Mtext([],":"); term2pres decl.Con.dec_type]) in + let suchthat = + P.Mrow ([], + [P.Mtext([None,"mathcolor","Red"],"such that"); + P.smallskip; + P.Mtext([],"("); + P.Mi([],get_name hyp); + P.Mtext([],")"); + P.smallskip; + term2pres hyp.Con.dec_type]) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + let body = conclude2pres proof.Con.proof_conclude false true in + let presacontext = + acontext2pres proof.Con.proof_apply_context body false in + P.Mtable + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr ([],[P.Mtd ([],presdecl)]); + P.Mtr ([],[P.Mtd ([],suchthat)]); + P.Mtr ([],[P.Mtd ([],presacontext)])]); + | _ -> assert false in proof2pres p ;; @@ -693,7 +809,7 @@ let content2pres term2pres (id,params,metasenv,obj) = (id,n,context,ty) -> P.Mtr [] [P.Mtd [] - (P.Mrow [] + (P.Mrow [Some "helm", "xref", id] (List.map (function (_,None) ->