From 6dcc9b0709d999e742721da8a9f5070d8faa6835 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 May 2007 15:06:22 +0000 Subject: [PATCH] DOOMSDAY 1.0: this is the commit that (partially) allows Matita to understand its own output. I.e. the natural language generated is now the declarative language. This is probably still highly bugged in most cases. --- components/content_pres/content2pres.ml | 198 ++++++++++++++---------- 1 file changed, 112 insertions(+), 86 deletions(-) diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml index a8b0bc6a0..e377706b7 100644 --- a/components/content_pres/content2pres.ml +++ b/components/content_pres/content2pres.ml @@ -100,10 +100,10 @@ let make_args_for_apply term2pres args = | Con.Term t -> if is_first then (term2pres t)::row - else (B.b_object (P.Mi([],"_")))::row + else (B.b_object (P.Mi([],"?")))::row | Con.ArgProof _ | Con.ArgMethod _ -> - (B.b_object (P.Mi([],"_")))::row + (B.b_object (P.Mi([],"?")))::row in if is_first then res else B.skip::res in @@ -132,10 +132,10 @@ let rec justification term2pres p = (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 term2pres p]) + Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p]) -and proof2pres term2pres p = - let rec proof2pres p = +and proof2pres is_top_down term2pres p = + let rec proof2pres is_top_down p omit_dot = let indent = let is_decl e = (match e with @@ -150,10 +150,16 @@ and proof2pres term2pres p = | Some t -> Some (term2pres t)) in let body = let presconclude = - conclude2pres p.Con.proof_conclude indent omit_conclusion in + conclude2pres is_top_down p.Con.proof_conclude indent omit_conclusion + omit_dot in let presacontext = - acontext2pres p.Con.proof_apply_context presconclude indent in - context2pres p.Con.proof_context presacontext in + acontext2pres + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + p.Con.proof_apply_context presconclude indent + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + in + context2pres p.Con.proof_context presacontext + in match p.Con.proof_name with None -> body | Some name -> @@ -166,9 +172,7 @@ and proof2pres term2pres p = "proof of" ac in B.b_toggle [ concl; body ] in - B.V ([], - [B.Text ([],"(" ^ name ^ ")"); - B.indent action]) + B.indent action and context2pres c continuation = (* we generate a subtable for each context element, for selection @@ -202,82 +206,93 @@ and proof2pres term2pres p = and ce2pres_in_proof_context_element = function | `Joint ho -> B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs)) - | (`Declaration _) as x -> ce2pres x - | (`Hypothesis _) as x -> ce2pres x + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x | (`Proof _) as x -> ce2pres x - | (`Definition _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x - and ce2pres = + and ce2pres = function `Declaration d -> let ty = term2pres d.Con.dec_type in B.H ([], - [(B.b_kw "Assume"); + [(B.b_kw "assume"); B.b_space; B.Object ([], P.Mi([],get_name d.Con.dec_name)); B.Text([],":"); - ty]) + ty; + B.Text([],".")]) | `Hypothesis h -> let ty = term2pres h.Con.dec_type in B.H ([], - [(B.b_kw "Suppose"); + [(B.b_kw "suppose"); + B.b_space; + ty; B.b_space; B.Text([],"("); B.Object ([], P.Mi ([],get_name h.Con.dec_name)); B.Text([],")"); - B.b_space; - ty]) + B.Text([],".")]) | `Proof p -> - proof2pres p + proof2pres false p false | `Definition d -> let term = term2pres d.Con.def_term in B.H ([], - [ B.b_kw "Let"; B.b_space; + [ B.b_kw "let"; B.b_space; B.Object ([], P.Mi([],get_name d.Con.def_name)); - B.Text([]," = "); + B.Text([],Utf8Macro.unicode_of_tex "\\def"); term]) - and acontext2pres ac continuation indent = + and acontext2pres is_top_down ac continuation indent in_bu_conversion = List.fold_right (fun p continuation -> - let hd = - if indent then - B.indent (proof2pres p) - else - proof2pres p 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 - and conclude2pres conclude indent omit_conclusion = + and conclude2pres is_top_down conclude indent omit_conclusion omit_dot = let tconclude_body = match conclude.Con.conclude_conclusion with - Some t when - not omit_conclusion or + Some t (*when not omit_conclusion or (* CSC: I ignore the omit_conclusion flag in this case. *) (* CSC: Is this the correct behaviour? In the stylesheets *) (* CSC: we simply generated nothing (i.e. the output type *) (* CSC: of the function should become an option. *) - conclude.Con.conclude_method = "BU_Conversion" -> - let concl = (term2pres t) in + conclude.Con.conclude_method = "BU_Conversion" *) -> + let concl = term2pres t in if conclude.Con.conclude_method = "BU_Conversion" then - make_concl "that is equivalent to" concl + B.b_hv [] + (make_concl "that is equivalent to" concl :: + if is_top_down then [B.b_space ; B.Text([],"done.")] else []) else if conclude.Con.conclude_method = "FalseInd" then (* false ind is in charge to add the conclusion *) falseind conclude else let conclude_body = conclude_aux conclude 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 - B.V ([], [conclude_body; ann_concl]) - | _ -> conclude_aux conclude in - if indent then - B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], - [tconclude_body])) - else - B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) + if conclude.Con.conclude_method = "Intros+LetTac" + || conclude.Con.conclude_method = "ByInduction" + || conclude.Con.conclude_method = "TD_Conversion" + then + B.Text([],"") + else if omit_conclusion then B.Text([],"done.") + 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.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else []) + in + B.V ([], [conclude_body; ann_concl]) + | _ -> conclude_aux conclude + in + if indent then + B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], + [tconclude_body])) + else + B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) and conclude_aux conclude = if conclude.Con.conclude_method = "TD_Conversion" then @@ -295,9 +310,10 @@ and proof2pres term2pres p = | Some c -> (term2pres c)) in B.V ([], - [make_concl "we must prove" expected; + [make_concl "we need to prove" expected; make_concl "or equivalently" synth; - proof2pres subproof]) + B.Text([],"."); + proof2pres true subproof false]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false else if conclude.Con.conclude_method = "Exact" then @@ -311,15 +327,13 @@ and proof2pres term2pres p = | err -> assert false) in (match conclude.Con.conclude_conclusion with None -> - B.b_h [] [B.b_kw "Consider"; B.b_space; arg] + B.b_h [] [B.b_kw "by"; B.b_space; arg] | Some c -> let conclusion = term2pres c in - make_row - [arg; B.b_space; B.b_kw "proves"] - conclusion + B.b_h [] [B.b_kw "by"; B.b_space; arg] ) else if conclude.Con.conclude_method = "Intros+LetTac" then (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2pres p + [Con.ArgProof p] -> proof2pres true p false | _ -> assert false) (* OLD CODE let conclusion = @@ -331,7 +345,7 @@ and proof2pres term2pres p = B.V ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [B.H([],[B.Object([],proof2pres p)]); + [B.H([],[B.Object([],proof2pres p false)]); B.H([],[B.Object([], (make_concl "we proved 1" conclusion))])]); | _ -> assert false) @@ -359,6 +373,7 @@ and proof2pres term2pres p = (match List.nth conclude.Con.conclude_args 5 with Con.Term t -> term2pres t | _ -> assert false) in +(* B.V ([], B.H ([],[ (B.b_kw "rewrite"); @@ -367,6 +382,7 @@ and proof2pres 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 _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = let j1,j2 = justification term2pres p in @@ -406,7 +422,7 @@ and proof2pres term2pres p = | Con.Premise prem -> B.b_kw "premise" | Con.Lemma lemma -> B.b_kw "lemma" | Con.Term t -> term2pres t - | Con.ArgProof p -> proof2pres p + | Con.ArgProof p -> proof2pres true p false | Con.ArgMethod s -> B.b_kw "method" and case conclude = @@ -466,7 +482,7 @@ and proof2pres term2pres p = (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:: (make_cases args_for_cases)) + B.V ([], induction_on::to_prove:: B.Text([],".")::(make_cases args_for_cases)) and make_cases l = List.map make_case l @@ -491,16 +507,18 @@ and proof2pres term2pres p = | `Hypothesis h -> let name = get_name h.Con.dec_name in [B.b_space; + B.Text([],"("); B.Object ([], P.Mi ([],name)); B.Text([],":"); - (term2pres h.Con.dec_type)] - | _ -> [B.Text ([],"???")]) in + (term2pres h.Con.dec_type); + B.Text([],")")] + | _ -> assert false (*[B.Text ([],"???")]*)) in dec@p) args [] in let pattern = B.H ([], - (B.b_kw "Case"::B.b_space::name::pattern_aux)@ + (B.b_kw "case"::B.b_space::name::pattern_aux)@ [B.b_space; - B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in + B.Text([], ".")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with None -> B.b_kw "No conclusion!!!" @@ -516,20 +534,22 @@ and proof2pres term2pres p = `Hypothesis h -> let name = (match h.Con.dec_name with - None -> "no name" + None -> "useless" | Some s -> s) in B.indent (B.H ([], - [B.Text([],"("); + [term2pres h.Con.dec_type; + B.b_space; + B.Text([],"("); B.Object ([], P.Mi ([],name)); B.Text([],")"); - B.b_space; - term2pres h.Con.dec_type])) + B.Text([],".")])) | _ -> 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 p.Con.proof_conclude true false in + let body = + conclude2pres true p.Con.proof_conclude true true false in let presacontext = let acontext_id = match p.Con.proof_apply_context with @@ -538,8 +558,12 @@ and proof2pres term2pres p = in B.Action([None,"type","toggle"], [ B.indent (add_xref acontext_id (B.b_kw "Proof")); - acontext2pres p.Con.proof_apply_context body true]) in - B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) + acontext2pres + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + 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]) | _ -> assert false and falseind conclude = @@ -567,7 +591,7 @@ and proof2pres 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} in *) + (* let body = proof2pres {proof with Con.proof_context = tl} false in *) make_row arg proof_conclusion and andind conclude = @@ -605,10 +629,11 @@ and proof2pres term2pres p = B.Text([],")"); B.skip; 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 body = proof2pres {proof with Con.proof_context = tl} false in *) + let body= conclude2pres false proof.Con.proof_conclude false true false in let presacontext = - acontext2pres proof.Con.proof_apply_context body false in + acontext2pres false proof.Con.proof_apply_context body false false + in B.V ([], [B.H ([],arg@[B.skip; B.b_kw "we have"]); @@ -644,10 +669,11 @@ and proof2pres term2pres p = B.Text([],")"); B.skip; 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 body = proof2pres {proof with Con.proof_context = tl} false in *) + let body= conclude2pres false proof.Con.proof_conclude false true false in let presacontext = - acontext2pres proof.Con.proof_apply_context body false in + acontext2pres false proof.Con.proof_apply_context body false false + in B.V ([], [presdecl; @@ -656,7 +682,7 @@ and proof2pres term2pres p = | _ -> assert false in - proof2pres p + proof2pres is_top_down p false exception ToDo @@ -707,7 +733,7 @@ let conjecture2pres term2pres (id, n, context, ty) = None -> "_" | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); - proof2pres term2pres p]) + proof2pres true term2pres p]) (List.rev context)) ] :: [ B.b_h [] [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); @@ -778,20 +804,21 @@ let content2pres term2pres (id,params,metasenv,obj) = let name = get_name p.Content.proof_name in B.b_v [Some "helm","xref","id"] - ([ B.b_h [] (B.b_kw ("Proof " ^ name) :: params2pres params); - B.b_kw "Thesis:"; - B.indent (term2pres thesis) ] @ + ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: params2pres params @ [B.b_kw ":"]); + B.indent (term2pres thesis) ; B.b_kw "." ] @ metasenv2pres term2pres metasenv @ - [proof2pres term2pres p]) + [proof2pres true term2pres p ; B.b_kw "qed."]) | `Def (_, ty, `Definition body) -> let name = get_name body.Content.def_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params); - B.b_kw "Type:"; + ([B.b_h [] + (B.b_kw ("definition " ^ name) :: params2pres params @ [B.b_kw ":"]); B.indent (term2pres ty)] @ metasenv2pres term2pres metasenv @ - [B.b_kw "Body:"; term2pres body.Content.def_term]) + [B.b_kw ":="; + B.indent (term2pres body.Content.def_term); + B.b_kw "."]) | `Decl (_, `Declaration decl) | `Decl (_, `Hypothesis decl) -> let name = get_name decl.Content.dec_name in @@ -809,11 +836,10 @@ let content2pres term2pres (id,params,metasenv,obj) = let content2pres ~ids_to_inner_sorts = content2pres - (fun annterm -> + (fun ?(prec=90) annterm -> let ast, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in - CicNotationPres.box_of_mpres - (CicNotationPres.render ids_to_uris + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris ~prec (TermContentPres.pp_ast ast))) - -- 2.39.2