From 45bc31f244e06f1eead7c35bc5b812574edf1737 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 Jul 2003 15:43:35 +0000 Subject: [PATCH] Added Method "exists". --- .../ocaml/cic_transformations/content2pres.ml | 69 +++++++++++++++---- 1 file changed, 57 insertions(+), 12 deletions(-) diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 1616c21c8..04be41c45 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -297,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 -> @@ -409,6 +413,8 @@ 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 = "Rewrite") then let justif = (match (List.nth conclude.Con.conclude_args 6) with @@ -551,16 +557,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 @@ -646,7 +643,55 @@ and proof2pres term2pres p = None,"columnalign","left"], pattern::asubconcl::induction_hypothesis@ [P.Mtr([],[P.Mtd([],presacontext)])]) - | _ -> assert false in + | _ -> 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 ;; -- 2.39.2