From 60f8a4de1287ea04ee5722460bdc6ff16a3eb4be Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 29 Jul 2003 09:53:53 +0000 Subject: [PATCH] Added method AndInd. --- helm/ocaml/cic_omdoc/cic2content.ml | 5 +- .../ocaml/cic_transformations/content2pres.ml | 68 ++++++++++++++++++- .../cic_transformations/mpresentation.ml | 4 +- 3 files changed, 71 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 0933dbc4b..0295daac3 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -699,8 +699,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = if n<0 then raise NotApplicable else let method_name = - if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then - "Exists" + if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or + uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists" + else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd" else "ByInduction" in let prefix = String.sub uri_str 0 n in let ind_str = (prefix ^ ".ind") in diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 04be41c45..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 = @@ -342,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)]); @@ -415,6 +418,8 @@ and proof2pres term2pres p = 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 @@ -645,6 +650,65 @@ and proof2pres term2pres p = [P.Mtr([],[P.Mtd([],presacontext)])]) | _ -> 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 diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 34c65a417..3c4f92902 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -207,7 +207,7 @@ and print_mrow = and print_mtd = let module X = Xml in function - Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr (print_mpres m) + Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr [< (print_mpres m) ; X.xml_nempty ~prefix "mphantom" [] (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >] ;; let print_mpres pres = @@ -217,7 +217,7 @@ let print_mpres pres = [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; Some "xmlns","helm","http://www.cs.unibo.it/helm" ; Some "xmlns","xlink","http://www.w3.org/1999/xlink" - ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"] (print_mpres pres)) + ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres)) >] -- 2.39.2